Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpt2bi123f Structured version   Visualization version   GIF version

Theorem mpt2bi123f 34281
Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mpt2bi123f.1 𝑥𝐴
mpt2bi123f.2 𝑥𝐵
mpt2bi123f.3 𝑦𝐴
mpt2bi123f.4 𝑦𝐵
mpt2bi123f.5 𝑦𝐶
mpt2bi123f.6 𝑦𝐷
mpt2bi123f.7 𝑥𝐶
mpt2bi123f.8 𝑥𝐷
Assertion
Ref Expression
mpt2bi123f (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpt2bi123f
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpt2bi123f.1 . . . . . . . 8 𝑥𝐴
2 mpt2bi123f.2 . . . . . . . 8 𝑥𝐵
31, 2nfeq 2960 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2874 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2249 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 mpt2bi123f.3 . . . . . . . . . 10 𝑦𝐴
76nfcri 2942 . . . . . . . . 9 𝑦 𝑥𝐴
8 mpt2bi123f.4 . . . . . . . . . 10 𝑦𝐵
98nfcri 2942 . . . . . . . . 9 𝑦 𝑥𝐵
107, 9nfbi 1995 . . . . . . . 8 𝑦(𝑥𝐴𝑥𝐵)
11 ax-5 2001 . . . . . . . 8 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑥𝐴𝑥𝐵))
1210, 11alrimi 2249 . . . . . . 7 ((𝑥𝐴𝑥𝐵) → ∀𝑦𝑧(𝑥𝐴𝑥𝐵))
1312alimi 1896 . . . . . 6 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
145, 13syl 17 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
15 mpt2bi123f.5 . . . . . . . 8 𝑦𝐶
16 mpt2bi123f.6 . . . . . . . 8 𝑦𝐷
1715, 16nfeq 2960 . . . . . . 7 𝑦 𝐶 = 𝐷
18 eleq2 2874 . . . . . . 7 (𝐶 = 𝐷 → (𝑦𝐶𝑦𝐷))
1917, 18alrimi 2249 . . . . . 6 (𝐶 = 𝐷 → ∀𝑦(𝑦𝐶𝑦𝐷))
20 ax-5 2001 . . . . . . 7 ((𝑦𝐶𝑦𝐷) → ∀𝑧(𝑦𝐶𝑦𝐷))
2120alimi 1896 . . . . . 6 (∀𝑦(𝑦𝐶𝑦𝐷) → ∀𝑦𝑧(𝑦𝐶𝑦𝐷))
22 mpt2bi123f.7 . . . . . . . . . . 11 𝑥𝐶
2322nfcri 2942 . . . . . . . . . 10 𝑥 𝑦𝐶
24 mpt2bi123f.8 . . . . . . . . . . 11 𝑥𝐷
2524nfcri 2942 . . . . . . . . . 10 𝑥 𝑦𝐷
2623, 25nfbi 1995 . . . . . . . . 9 𝑥(𝑦𝐶𝑦𝐷)
2726nfal 2329 . . . . . . . 8 𝑥𝑧(𝑦𝐶𝑦𝐷)
2827nfal 2329 . . . . . . 7 𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)
2928nf5ri 2230 . . . . . 6 (∀𝑦𝑧(𝑦𝐶𝑦𝐷) → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
3019, 21, 293syl 18 . . . . 5 (𝐶 = 𝐷 → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
31 id 22 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) → ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3231alanimi 1901 . . . . . . 7 ((∀𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3332alanimi 1901 . . . . . 6 ((∀𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3433alanimi 1901 . . . . 5 ((∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3514, 30, 34syl2an 585 . . . 4 ((𝐴 = 𝐵𝐶 = 𝐷) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
36 eqeq2 2817 . . . . . . 7 (𝐸 = 𝐹 → (𝑧 = 𝐸𝑧 = 𝐹))
3736alrimiv 2018 . . . . . 6 (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹))
38372ralimi 3141 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
39 hbra1 3130 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
40 rsp 3117 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4139, 40alrimih 1908 . . . . . . . 8 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
42 19.21v 2031 . . . . . . . . 9 (∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4342albii 1904 . . . . . . . 8 (∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4441, 43sylibr 225 . . . . . . 7 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
4544ralimi 3140 . . . . . 6 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
46 hbra1 3130 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
47 rsp 3117 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
4846, 47alrimih 1908 . . . . . 6 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
49 19.21v 2031 . . . . . . . 8 (∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
50492albii 1905 . . . . . . 7 (∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
51719.21 2242 . . . . . . . 8 (∀𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5251albii 1904 . . . . . . 7 (∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5350, 52sylbbr 227 . . . . . 6 (∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5445, 48, 533syl 18 . . . . 5 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5538, 54syl 17 . . . 4 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
56 id 22 . . . . . . 7 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5756alanimi 1901 . . . . . 6 ((∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5857alanimi 1901 . . . . 5 ((∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5958alanimi 1901 . . . 4 ((∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
6035, 55, 59syl2an 585 . . 3 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
61 tsan2 34259 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦𝐶)))
6261ord 882 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦𝐶)))
63 tsan2 34259 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
6463a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
6562, 64cnf1dd 34203 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
66 tsbi2 34251 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6766ord 882 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6867a1dd 50 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
69 ax-1 6 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
7068, 69contrd 34210 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
7170a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
7265, 71cnf1dd 34203 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
73 idd 24 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐴))
74 tsan2 34259 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
7574ord 882 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
76 tsan2 34259 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
7776a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
7875, 77cnf1dd 34203 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
79 tsim2 34248 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8079a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
8178, 80cnf1dd 34203 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
82 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8381, 82contrd 34210 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴𝑥𝐵))
8483a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
85 tsbi3 34252 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8685a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8784, 86cnfn2dd 34206 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
8873, 87cnf1dd 34203 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
89 tsan2 34259 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷)))
9089a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷))))
9188, 90cnf1dd 34203 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦𝐷)))
92 tsan2 34259 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9392a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
9491, 93cnf1dd 34203 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9572, 94contrd 34210 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → 𝑥𝐴)
9695a1d 25 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐴))
97 ax-1 6 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
9879a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
9997, 98cnf2dd 34204 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
100 tsan3 34260 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
101100a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
10299, 101cnfn2dd 34206 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
10396, 102mpdd 43 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
104 notnotr 128 . . . . . . . . . . . . . . . . . 18 (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
105104a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
10692a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
107105, 106cnfn2dd 34206 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐵𝑦𝐷)))
108 tsan3 34260 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷)))
109108a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷))))
110107, 109cnfn2dd 34206 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐷))
111 tsan3 34260 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦𝐶𝑦𝐷) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
112111ord 882 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
11376a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
114112, 113cnf1dd 34203 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
11579a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
116114, 115cnf1dd 34203 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
117 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
118116, 117contrd 34210 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶𝑦𝐷))
119110, 118sylibrd 250 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐶))
12095a1d 25 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑥𝐴))
121 ax-1 6 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
12279a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
123121, 122cnf2dd 34204 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
124100a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
125123, 124cnfn2dd 34206 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
126120, 125mpdd 43 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
127119, 126mpdd 43 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸𝑧 = 𝐹)))
128120, 119jcad 504 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴𝑦𝐶)))
129 tsim3 34249 . . . . . . . . . . . . . . . . . . . 20 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
130129a1d 25 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
131121, 130cnf2dd 34204 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
132 tsbi1 34250 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
133132a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
134131, 133cnf2dd 34204 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
135105, 134cnfn2dd 34206 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
136 tsan1 34258 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
137136a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
138135, 137cnf2dd 34204 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸)))
139128, 138cnfn1dd 34205 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
140 tsan3 34260 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
141140a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
142105, 141cnfn2dd 34206 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
143 tsbi3 34252 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
144143a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
145144or32dd 34207 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
146142, 145cnfn2dd 34206 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
147139, 146cnf1dd 34203 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
148127, 147contrd 34210 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
149148a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
150129a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
15197, 150cnf2dd 34204 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
15266a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
153151, 152cnf2dd 34204 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
154149, 153cnf2dd 34204 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
15563a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
156154, 155cnfn2dd 34206 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴𝑦𝐶)))
157 tsan3 34260 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶)))
158157a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶))))
159156, 158cnfn2dd 34206 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐶))
160 tsan3 34260 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
161160a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
162154, 161cnfn2dd 34206 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
16396, 83sylibd 230 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐵))
164159, 118sylibd 230 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐷))
165163, 164jcad 504 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐵𝑦𝐷)))
166 tsan1 34258 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
167166a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
168149, 167cnf2dd 34204 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹)))
169165, 168cnfn1dd 34205 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
170 tsbi4 34253 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
171170a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
172171or32dd 34207 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
173169, 172cnf2dd 34204 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
174162, 173cnfn1dd 34205 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
175 tsim1 34247 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
176175a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
177176or32dd 34207 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ (𝑧 = 𝐸𝑧 = 𝐹))))
178174, 177cnf2dd 34204 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
179159, 178cnfn1dd 34205 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
180103, 179contrd 34210 . . . . . 6 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
181180efald2 34188 . . . . 5 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
182181alimi 1896 . . . 4 (∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
1831822alimi 1897 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
184 oprabbi 34280 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
18560, 183, 1843syl 18 . 2 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
186 df-mpt2 6879 . 2 (𝑥𝐴, 𝑦𝐶𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)}
187 df-mpt2 6879 . 2 (𝑥𝐵, 𝑦𝐷𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)}
188185, 186, 1873eqtr4g 2865 1 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  wal 1635   = wceq 1637  wfal 1650  wcel 2156  wnfc 2935  wral 3096  {coprab 6875  cmpt2 6876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-oprab 6878  df-mpt2 6879
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator