Main derivation
S01 · implies
Before
R=\{(1,2),(1,3),(3,3),(4,6)\}After
R\subseteq A\times B
Conditions: none
Rule: subset_def · Uses: G1, G2, subset_def, cartesian_product_def, roster_membership
Leaf basis: subset_def + cartesian_product_def + roster_membership
By the definition of subset, every element of R must lie in A×B. R is given by listing four ordered pairs; for each pair the first coordinate must be in A and the second in B: (1,2): 1∈A, 2∈B; (1,3): 1∈A, 3∈B; (3,3): 3∈A, 3∈B; (4,6): 4∈A, 6∈B. All four qualify, so R⊆A×B and R really is a binary relation from A to B.
S02 · equivalent
Before
x\in\mathrm{Dom}(R)After
x\in A\ \land\ \exists y\in B:\ (x,y)\in R
Conditions: none
Rule: mko_relation_def · Uses: mko_relation_def, S01
Leaf basis: mko_relation_def + set_builder
By the MKO, Dom(R)={x∈A ∣ there exists y∈B with (x,y)∈R}. By set-builder notation, x∈Dom(R) exactly when x∈A and some y∈B has (x,y)∈R. Dom(R) is determined by the data of R; it is not another name for the declared source A.
S03 · implies
Before
(1,2)\in R,\ (3,3)\in R,\ (4,6)\in R
After
1,3,4\in\mathrm{Dom}(R)Conditions: none
Rule: exists_intro · Uses: S02, G2, exists_intro
Leaf basis: exists_intro + set_builder
Find witnesses: (1,2)∈R gives the witness y=2 for x=1; (3,3)∈R gives y=3 for x=3; (4,6)∈R gives y=6 for x=4. The witnesses are in B and 1, 3, 4 are in A, so by ∃-introduction and S02, 1, 3, 4∈Dom(R). 1 has a second witness y=3, but one is enough.
S04 · implies
Before
y\in B,\quad (2,y)\in R\ ?
After
\forall y\in B:\ (2,y)\notin R
Conditions: none
Rule: cartesian_product_def · Uses: G2, roster_membership, cartesian_product_def, forall_intro
Leaf basis: roster_membership + cartesian_product_def + forall_intro + case_analysis
Take any y∈B. By the listing, (2,y)∈R exactly when (2,y) equals one of (1,2), (1,3), (3,3), (4,6). Equal ordered pairs need equal first coordinates, i.e. 2=1, 2=1, 2=3 or 2=4, all false (N2 checks this with the product (2−1)(2−1)(2−3)(2−4)≠0). So (2,y)∉R; since y is arbitrary, ∀-introduction gives the conclusion.
S05 · implies
Before
\forall y\in B:\ (2,y)\notin R
After
2\notin\mathrm{Dom}(R)Conditions: none
Rule: quantifier_negation · Uses: S02, S04, quantifier_negation
Leaf basis: quantifier_negation + set_builder
By quantifier negation, ∀y∈B (2,y)∉R is equivalent to ¬∃y∈B (2,y)∈R. By S02, 2∈Dom(R) would need such a y, so 2∉Dom(R). 2 belongs to the declared source A but has no outgoing pair at all.
S06 · implies
Before
1,3,4\in\mathrm{Dom}(R),\ 2\notin\mathrm{Dom}(R),\ \mathrm{Dom}(R)\subseteq AAfter
\mathrm{Dom}(R)=\{1,3,4\}\neq AConditions: none
Rule: set_extensionality · Uses: S03, S05, G1, set_extensionality
Leaf basis: set_extensionality + subset_def + roster_membership
⊇: S03. ⊆: Dom(R)⊆A={1,2,3,4}, and 2 is excluded by S05, so the elements of Dom(R) can only be 1, 3, 4. By set equality, Dom(R)={1,3,4}. Since 2∈A∖Dom(R), Dom(R)≠A.
S07 · implies
Before
2\notin\mathrm{Dom}(R),\ (1,2)\in R,\ (1,3)\in RAfter
R\ \text{is not a function}\ A\to BConditions: none
Rule: function_graph · Uses: S05, G2, function_graph
Leaf basis: function_graph + numeric_evaluation
A function A→B requires exactly one y for each x∈A. R fails in two places: 2 has no y at all (S05, not total), and 1 has two values, 2 and 3, with 2≠3 (not single-valued). Either failure alone is enough. MKO paragraph one notes that a relation need not be a total function.
S08 · implies
Before
y\in R[C],\quad C=\{1,3\}After
2\in R[C],\ 3\in R[C]
Conditions: none
Rule: mko_relation_def · Uses: mko_relation_def, G2, G3, exists_intro
Leaf basis: mko_relation_def + exists_intro + set_builder
By the MKO, y∈R[C] exactly when y∈B and some x∈C has (x,y)∈R. The pairs with first coordinate in C={1,3} are (1,2), (1,3), (3,3), giving the outputs 2, 3, 3. By ∃-introduction, 2∈R[C] (witness x=1) and 3∈R[C] (witness x=1 or x=3).
S09 · implies
Before
2,3\in R[C]
After
R[C]=\{2,3\}Conditions: none
Rule: set_extensionality · Uses: S08, G2, G3, set_extensionality
Leaf basis: set_extensionality + roster_membership + cartesian_product_def
⊆: the other elements of B are 4, 5, 6. No pair of R has second coordinate 4 or 5; the only pair with second coordinate 6 is (4,6), whose first coordinate 4∉C (N4: (4−1)(4−3)≠0). So 4, 5, 6∉R[C]. With S08, R[C]={2,3}. The output 3 occurs twice (from (1,3) and (3,3)) but is listed once in the set.
S10 · implies
Before
R[\varnothing]
After
R[\varnothing]=\varnothing
Conditions: none
Rule: mko_relation_def · Uses: mko_relation_def, empty_set_def
Leaf basis: mko_relation_def + empty_set_def + quantifier_negation + set_extensionality
y∈R[∅] would need some x∈∅ with (x,y)∈R; ∅ has no elements, so this fails for every y, and R[∅]=∅. This is what MKO paragraph two says: the image of the empty input set is empty.
S11 · implies
Before
R=\{(1,2),(1,3),(3,3),(4,6)\}After
R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\}\subseteq B\times AConditions: none
Rule: mko_relation_def · Uses: mko_relation_def, G2, L_converse_member
Leaf basis: mko_relation_def + cartesian_product_def + set_extensionality
By the MKO, R⁻¹={(y,x) ∣ (x,y)∈R}: reverse each pair. (1,2)→(2,1), (1,3)→(3,1), (3,3)→(3,3), (4,6)→(6,4). The first coordinates 2, 3, 3, 6 are in B and the second coordinates 1, 1, 3, 4 are in A, so R⁻¹⊆B×A: source and target are swapped as well. By L_converse_member, R⁻¹ consists of exactly these four pairs.
S12 · implies
Before
(1,2)\in R,\ (2,1)\in R^{-1}After
(2,1)\notin R,\ \text{so}\ R^{-1}\neq RConditions: none
Rule: set_extensionality · Uses: S01, S11, set_extensionality
Leaf basis: set_extensionality + cartesian_product_def + subset_def
Ordered pairs keep their direction: (2,1)∈R⁻¹ but (2,1)∉R, because R⊆A×B (S01) while the second coordinate 1∉B. By set equality, R⁻¹≠R. Although A and B share the labels 2, 3, 4, (1,2) and (2,1) are still different ordered pairs.
S13 · theorem_application
Before
\mathrm{Dom}(R^{-1})After
\mathrm{Dom}(R^{-1})=R[A]=\{2,3,6\}Conditions: none
Rule: L_dom_converse · Uses: S11, L_dom_converse
Leaf basis: mko_relation_def + set_extensionality + exists_intro
By Lemma L_dom_converse, Dom(R⁻¹)=R[A]. Compute R[A]: all four pairs of R have first coordinate in A, so all count, with outputs 2, 3, 3, 6, giving the set {2,3,6}. Direct check: the first coordinates of the pairs of R⁻¹ are 2, 3, 3, 6, in agreement. The elements 4 and 5 of B are not among them.
S14 · implies
Before
R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\}After
R^{-1}\ \text{is not a function}\ B\to AConditions: none
Rule: function_graph · Uses: S11, S13, function_graph
Leaf basis: function_graph + roster_membership
A function B→A requires exactly one x for each y∈B. 4∈B is not in Dom(R⁻¹)={2,3,6} (N5) and has no x at all; 3 has two values of x, namely 1 and 3. So R⁻¹ is not a function. The converse relation always exists, but it is not automatically an inverse function and gives no proof of injectivity, surjectivity or invertibility (MKO paragraph three).
S15 · theorem_application
Before
(R^{-1})^{-1}After
(R^{-1})^{-1}=RConditions: none
Rule: L_converse_twice · Uses: S11, L_converse_twice
Leaf basis: mko_relation_def + set_extensionality
By Lemma L_converse_twice, swapping again returns R: (2,1)→(1,2), (3,1)→(1,3), (3,3)→(3,3), (6,4)→(4,6), exactly the four pairs of R. Taking the converse can be undone at the level of relations, regardless of whether R⁻¹ is a function.
S16 · implies
Before
\text{S01, S06, S07, S09, S10, S11, S13, S14}After
\mathrm{Dom}(R)=\{1,3,4\},\ R[C]=\{2,3\},\ R[\varnothing]=\varnothing,\ \mathrm{Dom}(R^{-1})=\{2,3,6\}Conditions: none
Rule: and_intro_elim · Uses: S01, S06, S07, S09, S10, S11, S13, S14
Leaf basis: and_intro_elim
Summary: R⊆A×B (S01); Dom(R)={1,3,4}≠A (S06); R is not a function A→B (S07); R[C]={2,3} (S09); R[∅]=∅ (S10); R⁻¹={(2,1),(3,1),(3,3),(6,4)}⊆B×A (S11); Dom(R⁻¹)=R[A]={2,3,6} (S13); R⁻¹ is not a function B→A (S14).