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 33638
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 2772 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2687 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2080 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 mpt2bi123f.3 . . . . . . . . . 10 𝑦𝐴
76nfcri 2755 . . . . . . . . 9 𝑦 𝑥𝐴
8 mpt2bi123f.4 . . . . . . . . . 10 𝑦𝐵
98nfcri 2755 . . . . . . . . 9 𝑦 𝑥𝐵
107, 9nfbi 1830 . . . . . . . 8 𝑦(𝑥𝐴𝑥𝐵)
11 ax-5 1836 . . . . . . . 8 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑥𝐴𝑥𝐵))
1210, 11alrimi 2080 . . . . . . 7 ((𝑥𝐴𝑥𝐵) → ∀𝑦𝑧(𝑥𝐴𝑥𝐵))
1312alimi 1736 . . . . . 6 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
145, 13syl 17 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
15 mpt2bi123f.5 . . . . . . . 8 𝑦𝐶
16 mpt2bi123f.6 . . . . . . . 8 𝑦𝐷
1715, 16nfeq 2772 . . . . . . 7 𝑦 𝐶 = 𝐷
18 eleq2 2687 . . . . . . 7 (𝐶 = 𝐷 → (𝑦𝐶𝑦𝐷))
1917, 18alrimi 2080 . . . . . 6 (𝐶 = 𝐷 → ∀𝑦(𝑦𝐶𝑦𝐷))
20 ax-5 1836 . . . . . . 7 ((𝑦𝐶𝑦𝐷) → ∀𝑧(𝑦𝐶𝑦𝐷))
2120alimi 1736 . . . . . 6 (∀𝑦(𝑦𝐶𝑦𝐷) → ∀𝑦𝑧(𝑦𝐶𝑦𝐷))
22 mpt2bi123f.7 . . . . . . . . . . 11 𝑥𝐶
2322nfcri 2755 . . . . . . . . . 10 𝑥 𝑦𝐶
24 mpt2bi123f.8 . . . . . . . . . . 11 𝑥𝐷
2524nfcri 2755 . . . . . . . . . 10 𝑥 𝑦𝐷
2623, 25nfbi 1830 . . . . . . . . 9 𝑥(𝑦𝐶𝑦𝐷)
2726nfal 2150 . . . . . . . 8 𝑥𝑧(𝑦𝐶𝑦𝐷)
2827nfal 2150 . . . . . . 7 𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)
2928nf5ri 2063 . . . . . 6 (∀𝑦𝑧(𝑦𝐶𝑦𝐷) → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
3019, 21, 293syl 18 . . . . 5 (𝐶 = 𝐷 → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
31 id 22 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) → ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3231alanimi 1741 . . . . . . 7 ((∀𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3332alanimi 1741 . . . . . 6 ((∀𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3433alanimi 1741 . . . . 5 ((∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3514, 30, 34syl2an 494 . . . 4 ((𝐴 = 𝐵𝐶 = 𝐷) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
36 eqeq2 2632 . . . . . . 7 (𝐸 = 𝐹 → (𝑧 = 𝐸𝑧 = 𝐹))
3736alrimiv 1852 . . . . . 6 (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹))
38372ralimi 2948 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
39 hbra1 2937 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
40 rsp 2924 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4139, 40alrimih 1748 . . . . . . . 8 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
42 19.21v 1865 . . . . . . . . 9 (∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4342albii 1744 . . . . . . . 8 (∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4441, 43sylibr 224 . . . . . . 7 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
4544ralimi 2947 . . . . . 6 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
46 hbra1 2937 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
47 rsp 2924 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
4846, 47alrimih 1748 . . . . . 6 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
49 19.21v 1865 . . . . . . . 8 (∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
50492albii 1745 . . . . . . 7 (∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
51719.21 2073 . . . . . . . 8 (∀𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5251albii 1744 . . . . . . 7 (∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5350, 52sylbbr 226 . . . . . 6 (∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5445, 48, 533syl 18 . . . . 5 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5538, 54syl 17 . . . 4 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
56 id 22 . . . . . . 7 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5756alanimi 1741 . . . . . 6 ((∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5857alanimi 1741 . . . . 5 ((∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5958alanimi 1741 . . . 4 ((∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
6035, 55, 59syl2an 494 . . 3 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
61 tsan2 33616 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦𝐶)))
6261ord 392 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦𝐶)))
63 tsan2 33616 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
6463a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
6562, 64cnf1dd 33559 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
66 tsbi2 33608 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6766ord 392 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6867a1dd 50 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
69 ax-1 6 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
7068, 69contrd 33566 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
7170a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
7265, 71cnf1dd 33559 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
73 idd 24 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐴))
74 tsan2 33616 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
7574ord 392 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
76 tsan2 33616 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
7776a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
7875, 77cnf1dd 33559 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
79 tsim2 33605 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8079a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
8178, 80cnf1dd 33559 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
82 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8381, 82contrd 33566 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴𝑥𝐵))
8483a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
85 tsbi3 33609 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8685a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8784, 86cnfn2dd 33562 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
8873, 87cnf1dd 33559 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
89 tsan2 33616 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷)))
9089a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷))))
9188, 90cnf1dd 33559 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦𝐷)))
92 tsan2 33616 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9392a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
9491, 93cnf1dd 33559 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9572, 94contrd 33566 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → 𝑥𝐴)
9695a1d 25 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐴))
97 ax-1 6 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
9879a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
9997, 98cnf2dd 33560 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
100 tsan3 33617 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
101100a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
10299, 101cnfn2dd 33562 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
10396, 102mpdd 43 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
104 notnotr 125 . . . . . . . . . . . . . . . . . 18 (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
105104a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
10692a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
107105, 106cnfn2dd 33562 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐵𝑦𝐷)))
108 tsan3 33617 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷)))
109108a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷))))
110107, 109cnfn2dd 33562 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐷))
111 tsan3 33617 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦𝐶𝑦𝐷) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
112111ord 392 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
11376a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
114112, 113cnf1dd 33559 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
11579a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
116114, 115cnf1dd 33559 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
117 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
118116, 117contrd 33566 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶𝑦𝐷))
119110, 118sylibrd 249 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐶))
12095a1d 25 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑥𝐴))
121 ax-1 6 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
12279a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
123121, 122cnf2dd 33560 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
124100a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
125123, 124cnfn2dd 33562 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
126120, 125mpdd 43 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
127119, 126mpdd 43 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸𝑧 = 𝐹)))
128120, 119jcad 555 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴𝑦𝐶)))
129 tsim3 33606 . . . . . . . . . . . . . . . . . . . 20 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
130129a1d 25 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
131121, 130cnf2dd 33560 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
132 tsbi1 33607 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
133132a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
134131, 133cnf2dd 33560 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
135105, 134cnfn2dd 33562 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
136 tsan1 33615 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
137136a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
138135, 137cnf2dd 33560 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸)))
139128, 138cnfn1dd 33561 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
140 tsan3 33617 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
141140a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
142105, 141cnfn2dd 33562 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
143 tsbi3 33609 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
144143a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
145144or32dd 33563 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
146142, 145cnfn2dd 33562 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
147139, 146cnf1dd 33559 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
148127, 147contrd 33566 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
149148a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
150129a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
15197, 150cnf2dd 33560 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
15266a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
153151, 152cnf2dd 33560 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
154149, 153cnf2dd 33560 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
15563a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
156154, 155cnfn2dd 33562 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴𝑦𝐶)))
157 tsan3 33617 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶)))
158157a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶))))
159156, 158cnfn2dd 33562 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐶))
160 tsan3 33617 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
161160a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
162154, 161cnfn2dd 33562 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
16396, 83sylibd 229 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐵))
164159, 118sylibd 229 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐷))
165163, 164jcad 555 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐵𝑦𝐷)))
166 tsan1 33615 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
167166a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
168149, 167cnf2dd 33560 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹)))
169165, 168cnfn1dd 33561 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
170 tsbi4 33610 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
171170a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
172171or32dd 33563 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
173169, 172cnf2dd 33560 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
174162, 173cnfn1dd 33561 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
175 tsim1 33604 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
176175a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
177176or32dd 33563 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ (𝑧 = 𝐸𝑧 = 𝐹))))
178174, 177cnf2dd 33560 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
179159, 178cnfn1dd 33561 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
180103, 179contrd 33566 . . . . . 6 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
181180efald2 33544 . . . . 5 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
182181alimi 1736 . . . 4 (∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
1831822alimi 1737 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
184 oprabbi 33637 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
18560, 183, 1843syl 18 . 2 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
186 df-mpt2 6615 . 2 (𝑥𝐴, 𝑦𝐶𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)}
187 df-mpt2 6615 . 2 (𝑥𝐵, 𝑦𝐷𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)}
188185, 186, 1873eqtr4g 2680 1 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  wal 1478   = wceq 1480  wfal 1485  wcel 1987  wnfc 2748  wral 2907  {coprab 6611  cmpt2 6612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-oprab 6614  df-mpt2 6615
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator