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 33141
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 2762 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2677 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2069 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 mpt2bi123f.3 . . . . . . . . . 10 𝑦𝐴
76nfcri 2745 . . . . . . . . 9 𝑦 𝑥𝐴
8 mpt2bi123f.4 . . . . . . . . . 10 𝑦𝐵
98nfcri 2745 . . . . . . . . 9 𝑦 𝑥𝐵
107, 9nfbi 1821 . . . . . . . 8 𝑦(𝑥𝐴𝑥𝐵)
11 ax-5 1827 . . . . . . . 8 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑥𝐴𝑥𝐵))
1210, 11alrimi 2069 . . . . . . 7 ((𝑥𝐴𝑥𝐵) → ∀𝑦𝑧(𝑥𝐴𝑥𝐵))
1312alimi 1730 . . . . . 6 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
145, 13syl 17 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
15 mpt2bi123f.5 . . . . . . . 8 𝑦𝐶
16 mpt2bi123f.6 . . . . . . . 8 𝑦𝐷
1715, 16nfeq 2762 . . . . . . 7 𝑦 𝐶 = 𝐷
18 eleq2 2677 . . . . . . 7 (𝐶 = 𝐷 → (𝑦𝐶𝑦𝐷))
1917, 18alrimi 2069 . . . . . 6 (𝐶 = 𝐷 → ∀𝑦(𝑦𝐶𝑦𝐷))
20 ax-5 1827 . . . . . . 7 ((𝑦𝐶𝑦𝐷) → ∀𝑧(𝑦𝐶𝑦𝐷))
2120alimi 1730 . . . . . 6 (∀𝑦(𝑦𝐶𝑦𝐷) → ∀𝑦𝑧(𝑦𝐶𝑦𝐷))
22 mpt2bi123f.7 . . . . . . . . . . 11 𝑥𝐶
2322nfcri 2745 . . . . . . . . . 10 𝑥 𝑦𝐶
24 mpt2bi123f.8 . . . . . . . . . . 11 𝑥𝐷
2524nfcri 2745 . . . . . . . . . 10 𝑥 𝑦𝐷
2623, 25nfbi 1821 . . . . . . . . 9 𝑥(𝑦𝐶𝑦𝐷)
2726nfal 2139 . . . . . . . 8 𝑥𝑧(𝑦𝐶𝑦𝐷)
2827nfal 2139 . . . . . . 7 𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)
2928nf5ri 2053 . . . . . 6 (∀𝑦𝑧(𝑦𝐶𝑦𝐷) → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
3019, 21, 293syl 18 . . . . 5 (𝐶 = 𝐷 → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
31 id 22 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) → ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3231alanimi 1734 . . . . . . 7 ((∀𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3332alanimi 1734 . . . . . 6 ((∀𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3433alanimi 1734 . . . . 5 ((∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3514, 30, 34syl2an 493 . . . 4 ((𝐴 = 𝐵𝐶 = 𝐷) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
36 eqeq2 2621 . . . . . . . 8 (𝐸 = 𝐹 → (𝑧 = 𝐸𝑧 = 𝐹))
3736alrimiv 1842 . . . . . . 7 (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹))
3837ralimi 2936 . . . . . 6 (∀𝑦𝐶 𝐸 = 𝐹 → ∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
3938ralimi 2936 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
40 hbra1 2926 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
41 rsp 2913 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4240, 41alrimih 1741 . . . . . . . 8 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
43 19.21v 1855 . . . . . . . . 9 (∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4443albii 1737 . . . . . . . 8 (∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4542, 44sylibr 223 . . . . . . 7 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
4645ralimi 2936 . . . . . 6 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
47 hbra1 2926 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
48 rsp 2913 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
4947, 48alrimih 1741 . . . . . 6 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
50 19.21v 1855 . . . . . . . 8 (∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
51502albii 1738 . . . . . . 7 (∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
52719.21 2062 . . . . . . . 8 (∀𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5352albii 1737 . . . . . . 7 (∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5451, 53sylbbr 225 . . . . . 6 (∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5546, 49, 543syl 18 . . . . 5 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5639, 55syl 17 . . . 4 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
57 id 22 . . . . . . 7 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5857alanimi 1734 . . . . . 6 ((∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5958alanimi 1734 . . . . 5 ((∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
6059alanimi 1734 . . . 4 ((∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
6135, 56, 60syl2an 493 . . 3 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
62 tsan2 33119 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦𝐶)))
6362ord 391 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦𝐶)))
64 tsan2 33119 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
6564a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
6663, 65cnf1dd 33062 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
67 tsbi2 33111 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6867ord 391 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6968a1dd 48 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
70 ax-1 6 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
7169, 70contrd 33069 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
7271a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
7366, 72cnf1dd 33062 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
74 idd 24 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐴))
75 tsan2 33119 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
7675ord 391 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
77 tsan2 33119 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
7877a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
7976, 78cnf1dd 33062 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
80 tsim2 33108 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8180a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
8279, 81cnf1dd 33062 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
83 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8482, 83contrd 33069 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴𝑥𝐵))
8584a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
86 tsbi3 33112 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8786a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8885, 87cnfn2dd 33065 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
8974, 88cnf1dd 33062 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
90 tsan2 33119 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷)))
9190a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷))))
9289, 91cnf1dd 33062 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦𝐷)))
93 tsan2 33119 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9493a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
9592, 94cnf1dd 33062 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9673, 95contrd 33069 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → 𝑥𝐴)
9796a1d 25 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐴))
98 ax-1 6 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
9980a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
10098, 99cnf2dd 33063 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
101 tsan3 33120 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
102101a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
103100, 102cnfn2dd 33065 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
10497, 103mpdd 42 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
105 notnotr 124 . . . . . . . . . . . . . . . . . 18 (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
106105a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
10793a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
108106, 107cnfn2dd 33065 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐵𝑦𝐷)))
109 tsan3 33120 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷)))
110109a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷))))
111108, 110cnfn2dd 33065 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐷))
112 tsan3 33120 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦𝐶𝑦𝐷) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
113112ord 391 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
11477a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
115113, 114cnf1dd 33062 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
11680a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
117115, 116cnf1dd 33062 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
118 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
119117, 118contrd 33069 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶𝑦𝐷))
120111, 119sylibrd 248 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐶))
12196a1d 25 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑥𝐴))
122 ax-1 6 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
12380a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
124122, 123cnf2dd 33063 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
125101a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
126124, 125cnfn2dd 33065 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
127121, 126mpdd 42 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
128120, 127mpdd 42 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸𝑧 = 𝐹)))
129121, 120jcad 554 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴𝑦𝐶)))
130 tsim3 33109 . . . . . . . . . . . . . . . . . . . 20 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
131130a1d 25 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
132122, 131cnf2dd 33063 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
133 tsbi1 33110 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
134133a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
135132, 134cnf2dd 33063 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
136106, 135cnfn2dd 33065 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
137 tsan1 33118 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
138137a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
139136, 138cnf2dd 33063 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸)))
140129, 139cnfn1dd 33064 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
141 tsan3 33120 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
142141a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
143106, 142cnfn2dd 33065 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
144 tsbi3 33112 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
145144a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
146145or32dd 33066 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
147143, 146cnfn2dd 33065 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
148140, 147cnf1dd 33062 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
149128, 148contrd 33069 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
150149a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
151130a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
15298, 151cnf2dd 33063 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
15367a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
154152, 153cnf2dd 33063 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
155150, 154cnf2dd 33063 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
15664a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
157155, 156cnfn2dd 33065 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴𝑦𝐶)))
158 tsan3 33120 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶)))
159158a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶))))
160157, 159cnfn2dd 33065 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐶))
161 tsan3 33120 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
162161a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
163155, 162cnfn2dd 33065 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
16497, 84sylibd 228 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐵))
165160, 119sylibd 228 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐷))
166164, 165jcad 554 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐵𝑦𝐷)))
167 tsan1 33118 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
168167a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
169150, 168cnf2dd 33063 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹)))
170166, 169cnfn1dd 33064 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
171 tsbi4 33113 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
172171a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
173172or32dd 33066 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
174170, 173cnf2dd 33063 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
175163, 174cnfn1dd 33064 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
176 tsim1 33107 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
177176a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
178177or32dd 33066 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ (𝑧 = 𝐸𝑧 = 𝐹))))
179175, 178cnf2dd 33063 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
180160, 179cnfn1dd 33064 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
181104, 180contrd 33069 . . . . . 6 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
182181efald2 33047 . . . . 5 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
183182alimi 1730 . . . 4 (∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
1841832alimi 1731 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
185 oprabbi 33140 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
18661, 184, 1853syl 18 . 2 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
187 df-mpt2 6554 . 2 (𝑥𝐴, 𝑦𝐶𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)}
188 df-mpt2 6554 . 2 (𝑥𝐵, 𝑦𝐷𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)}
189186, 187, 1883eqtr4g 2669 1 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  wal 1473   = wceq 1475  wfal 1480  wcel 1977  wnfc 2738  wral 2896  {coprab 6550  cmpt2 6551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-oprab 6553  df-mpt2 6554
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator