Main derivation
S01 · definition
Before
\text{multiples of }6,\ \text{even integers},\ \text{multiples of }4\ \text{in }\mathbb{Z}After
A=\{n\in\mathbb{Z}\mid\exists k\in\mathbb{Z},\ n=6k\},\ B=\{n\in\mathbb{Z}\mid\exists m\in\mathbb{Z},\ n=2m\},\ C=\{n\in\mathbb{Z}\mid\exists j\in\mathbb{Z},\ n=4j\}Conditions: none
Rule: def_intro · Uses: G1, G2
Leaf basis: def_intro + set_builder
Name the three sets with set-builder notation. All three consist of elements of ℤ, so they lie in the same universe ℤ, as MKO assumption a1 requires; only then is comparing them by inclusion meaningful. By set_builder, n∈A means exactly that n∈ℤ and n=6k for some integer k, and likewise for B and C.
S02 · equivalent
Before
A\subseteq B
After
\forall x\ (x\in A\Rightarrow x\in B)
Conditions: A,B\subseteq\mathbb{Z}
Rule: mko_subset_def · Uses: S01, mko_subset_def
Leaf basis: mko_subset_def + subset_def + def_unfold
Unfold the goal by the MKO's definition: A⊆B holds exactly when, for every object x, x∈A implies x∈B. For objects outside ℤ, x∈A is false and the implication holds automatically, so in effect only x∈ℤ needs checking. The step turns a statement about two sets into a universal statement about all elements; proving it requires handling an arbitrary x, not a few chosen elements.
S03 · equivalent
Before
x\in A\ \ (x\in\mathbb{Z}\ \text{arbitrary})After
\exists k\in\mathbb{Z},\ x=6kConditions: x\in\mathbb{Z}
Rule: set_builder · Uses: S01, S02
Leaf basis: set_builder + def_unfold
Take an arbitrary x∈ℤ and temporarily assume x∈A (this assumption is discharged in S07). By the set-builder definition of A, x∈A is equivalent to 'x=6k for some integer k'. Nothing is assumed about x beyond x∈ℤ and this temporary assumption.
S04 · implies
Before
\exists k\in\mathbb{Z},\ x=6kAfter
x=6k_0,\ k_0\in\mathbb{Z}Conditions: none
Rule: exists_elim · Uses: S03
Leaf basis: exists_elim
By ∃-elimination, give some integer with this property the fresh name k₀, so x=6k₀. k₀ only names that integer, and the final conclusion x∈B does not mention k₀, so this is allowed.
S05 · equivalent
Before
x=6k_0
After
x=2(3k_0)
Conditions: none
Rule: eq_replace · Uses: S04
Leaf basis: numeric_evaluation + mul_assoc + eq_replace
Write 6 as 2·3 and use associativity of multiplication: 6k₀=(2·3)k₀=2(3k₀). Both sides are the same integer, so the truth of the equation is unchanged. This is the only computation in the proof, and it holds for every k₀ (N1 checks it as a polynomial identity).
S06 · implies
Before
x=2(3k_0),\ k_0\in\mathbb{Z}After
x\in B
Conditions: 3k_0\in\mathbb{Z}
Rule: exists_intro · Uses: S04, S05, int_closure
Leaf basis: int_closure + exists_intro + set_builder
Since 3 and k₀ are integers, closure under multiplication gives 3k₀∈ℤ. So m=3k₀ is an integer with x=2m; by ∃-introduction and the set-builder definition of B, x∈B.
S07 · implies
Before
x\in A\ \text{assumed}\ \vdash\ x\in B,\quad x\in\mathbb{Z}\ \text{arbitrary}After
A\subseteq B
Conditions: none
Rule: forall_intro · Uses: S02, S03, S06
Leaf basis: imp_intro + forall_intro + def_unfold
First discharge the temporary assumption of S03 by →-introduction, giving x∈A⇒x∈B; from here on x∈A is no longer treated as known. S03 to S06 used only x∈ℤ and did not pick a particular x, so ∀-introduction gives ∀x∈ℤ (x∈A⇒x∈B); objects outside ℤ satisfy it automatically, as noted in S02. Folding the definition back by S02 gives A⊆B.
S08 · implies
Before
2=2\cdot 1,\quad 2\in A\iff\exists k\in\mathbb{Z},\ 6k=2After
2\in B,\ 2\notin A
Conditions: none
Rule: L_6k_ne_2 · Uses: S01
Leaf basis: set_builder + exists_intro + quantifier_negation + int_discrete + order_basics
2=2·1 with 1∈ℤ, so 2∈B. On the other hand, by the definition of A, 2∈A would need an integer k with 6k=2; Lemma L_6k_ne_2 (proved in S08.1 and S08.2) says there is no such integer, so by negating the quantifier, 2∉A.
S09 · implies
Before
A\subseteq B,\ 2\in B,\ 2\notin A
After
A\neq B,\ A\subsetneq B
Conditions: none
Rule: proper_subset_def · Uses: S07, S08
Leaf basis: set_extensionality + proper_subset_def + and_intro_elim
By the criterion for set equality, A=B would require the same elements; 2 is in B but not in A, so A≠B. Together with A⊆B from S07, the definition of proper subset gives A⊊B. Strictness is an extra fact proved here; it is not part of what A⊆B means.
S10 · equivalent
Before
B\subseteq B
After
\forall x\ (x\in B\Rightarrow x\in B)
Conditions: none
Rule: mko_subset_def · Uses: S01, mko_subset_def
Leaf basis: mko_subset_def + imp_intro + forall_intro
Apply the same definition with both sets equal to B: B⊆B is equivalent to 'for every x, x∈B⇒x∈B'. Every statement implies itself (assuming x∈B, the conclusion x∈B is that very assumption), so the right side holds and B⊆B holds. This shows that ⊆ is non-strict: inclusion holds when the two sets are equal, and A⊆B does not require A≠B.
S11 · equivalent
Before
\neg(A\subseteq C)
After
\exists x\ (x\in A\land x\notin C)
Conditions: none
Rule: quantifier_negation · Uses: S01, mko_subset_def
Leaf basis: mko_subset_def + quantifier_negation + neg_imp
To negate A⊆C, first write it by the definition as ¬∀x (x∈A⇒x∈C). Negating the quantifier gives ∃x ¬(x∈A⇒x∈C), and negating the implication gives ∃x (x∈A ∧ x∉C). So refuting inclusion needs just one counterexample: an element of A that is not in C.
S12 · implies
Before
6=6\cdot 1,\quad 6\in C\iff\exists j\in\mathbb{Z},\ 4j=6After
6\in A,\ 6\notin C
Conditions: none
Rule: L_4j_ne_6 · Uses: S01
Leaf basis: set_builder + exists_intro + quantifier_negation + int_discrete + order_basics
6=6·1 with 1∈ℤ, so 6∈A. By the definition of C, 6∈C would need an integer j with 4j=6; Lemma L_4j_ne_6 (proved in S12.1 and S12.2) says there is no such integer, so 6∉C.
S13 · implies
Before
6\in A\land 6\notin C
After
A\not\subseteq C
Conditions: none
Rule: exists_intro · Uses: S11, S12
Leaf basis: exists_intro + and_intro_elim + logic_chain
Take x=6 as the witness: S12 gives 6∈A and 6∉C, so ∃-introduction gives ∃x (x∈A ∧ x∉C); by the equivalence S11, A⊄C. One counterexample is enough to refute inclusion.
S14 · implies
Before
12=6\cdot 2,\ 12=4\cdot 3
After
12\in A\cap C\ \text{and yet}\ A\not\subseteq CConditions: none
Rule: set_operations_def · Uses: S01, S13
Leaf basis: set_builder + exists_intro + set_operations_def + numeric_evaluation
12=6·2 and 12=4·3 with integer witnesses 2 and 3, so 12∈A and 12∈C, that is 12∈A∩C. Yet S13 proved A⊄C. So finding a common element does not establish inclusion; inclusion is a requirement on every element of A.
S15 · equivalent
Before
\{6\}\subseteq AAfter
6\in A
Conditions: none
Rule: L_singleton_subset · Uses: S12
Leaf basis: singleton_def + subset_def + forall_elim + forall_intro + eq_replace
By Lemma L_singleton_subset (with S=A and a=6), {6}⊆A and 6∈A are true or false together; S12 proved 6∈A, so {6}⊆A holds as well. The two statements have the same truth value but are not the same statement: 6∈A compares an element with a set, while {6}⊆A compares two sets.
S16 · implies
Before
A\subseteq B,\ 2\in B\setminus A,\ 6\in A\setminus C,\ 6\in A
After
A\subsetneq B,\ A\not\subseteq C,\ B\subseteq B,\ \{6\}\subseteq AConditions: none
Rule: and_intro_elim · Uses: S07, S09, S10, S13, S14, S15
Leaf basis: and_intro_elim
Collect the results: A⊊B (S07, S09); A⊄C even though 12∈A∩C (S13, S14); B⊆B shows that ⊆ allows equality (S10); {6}⊆A and 6∈A are both true but play different type roles (S15).
Substeps and lemmas
S08.1 · case_split
Before
k\in\mathbb{Z}After
k\le 0\ \lor\ k\ge 1
Conditions: k\in\mathbb{Z}
Rule: int_discrete · Uses: int_discrete
Leaf basis: int_discrete + case_analysis
Let k be any integer. By discreteness of the integers (with c=0), k≤0 or k≥1, with no third possibility; the two cases cover every integer.
S08.2 · implies
Before
k\le 0\ \lor\ k\ge 1
After
6k\neq 2
Conditions: 6>0
Rule: case_analysis · Uses: S08.1, order_basics
Leaf basis: order_basics + case_analysis + forall_intro + numeric_evaluation
Case 1: k≤0. Multiplying by the positive number 6 gives 6k≤0<2, so 6k≠2. Case 2: k≥1. Multiplying by 6 gives 6k≥6>2, so 6k≠2. Both cases give 6k≠2, so proof by cases applies; since k was arbitrary, S08.1 and S08.2 together prove Lemma L_6k_ne_2.
S12.1 · case_split
Before
j\in\mathbb{Z}After
j\le 1\ \lor\ j\ge 2
Conditions: j\in\mathbb{Z}
Rule: int_discrete · Uses: int_discrete
Leaf basis: int_discrete + case_analysis
Let j be any integer. By discreteness of the integers (with c=1), j≤1 or j≥2, and the two cases cover every integer.
S12.2 · implies
Before
j\le 1\ \lor\ j\ge 2
After
4j\neq 6
Conditions: 4>0
Rule: case_analysis · Uses: S12.1, order_basics
Leaf basis: order_basics + case_analysis + forall_intro + numeric_evaluation
Case 1: j≤1; multiplying by 4>0 gives 4j≤4<6. Case 2: j≥2; multiplying by 4 gives 4j≥8>6. Both cases give 4j≠6; since j was arbitrary, S12.1 and S12.2 together prove Lemma L_4j_ne_6.
S15.1 · implies
Before
\{a\}\subseteq SAfter
a\in S
Conditions: none
Rule: forall_elim · Uses: singleton_def, subset_def
Leaf basis: singleton_def + eq_refl_symm_trans + subset_def + forall_elim
(⇒) By the definition of a singleton, a∈{a}, since a=a. {a}⊆S says every element of {a} is in S; instantiating this universal statement at x=a (∀-elimination) gives a∈S.
S15.2 · implies
Before
a\in S
After
\{a\}\subseteq SConditions: none
Rule: forall_intro · Uses: singleton_def, subset_def
Leaf basis: singleton_def + eq_replace + imp_intro + forall_intro + subset_def
(⇐) Suppose a∈S. Take an arbitrary x∈{a}; by the definition of a singleton x=a, and by replacement of equals x∈S. Since x was arbitrary, ∀-introduction and the subset definition give {a}⊆S. S15.1 and S15.2 together prove Lemma L_singleton_subset.