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 34303
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 2925 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2839 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2238 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 mpt2bi123f.3 . . . . . . . . . 10 𝑦𝐴
76nfcri 2907 . . . . . . . . 9 𝑦 𝑥𝐴
8 mpt2bi123f.4 . . . . . . . . . 10 𝑦𝐵
98nfcri 2907 . . . . . . . . 9 𝑦 𝑥𝐵
107, 9nfbi 1985 . . . . . . . 8 𝑦(𝑥𝐴𝑥𝐵)
11 ax-5 1991 . . . . . . . 8 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑥𝐴𝑥𝐵))
1210, 11alrimi 2238 . . . . . . 7 ((𝑥𝐴𝑥𝐵) → ∀𝑦𝑧(𝑥𝐴𝑥𝐵))
1312alimi 1887 . . . . . 6 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
145, 13syl 17 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
15 mpt2bi123f.5 . . . . . . . 8 𝑦𝐶
16 mpt2bi123f.6 . . . . . . . 8 𝑦𝐷
1715, 16nfeq 2925 . . . . . . 7 𝑦 𝐶 = 𝐷
18 eleq2 2839 . . . . . . 7 (𝐶 = 𝐷 → (𝑦𝐶𝑦𝐷))
1917, 18alrimi 2238 . . . . . 6 (𝐶 = 𝐷 → ∀𝑦(𝑦𝐶𝑦𝐷))
20 ax-5 1991 . . . . . . 7 ((𝑦𝐶𝑦𝐷) → ∀𝑧(𝑦𝐶𝑦𝐷))
2120alimi 1887 . . . . . 6 (∀𝑦(𝑦𝐶𝑦𝐷) → ∀𝑦𝑧(𝑦𝐶𝑦𝐷))
22 mpt2bi123f.7 . . . . . . . . . . 11 𝑥𝐶
2322nfcri 2907 . . . . . . . . . 10 𝑥 𝑦𝐶
24 mpt2bi123f.8 . . . . . . . . . . 11 𝑥𝐷
2524nfcri 2907 . . . . . . . . . 10 𝑥 𝑦𝐷
2623, 25nfbi 1985 . . . . . . . . 9 𝑥(𝑦𝐶𝑦𝐷)
2726nfal 2317 . . . . . . . 8 𝑥𝑧(𝑦𝐶𝑦𝐷)
2827nfal 2317 . . . . . . 7 𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)
2928nf5ri 2219 . . . . . 6 (∀𝑦𝑧(𝑦𝐶𝑦𝐷) → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
3019, 21, 293syl 18 . . . . 5 (𝐶 = 𝐷 → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
31 id 22 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) → ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3231alanimi 1892 . . . . . . 7 ((∀𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3332alanimi 1892 . . . . . 6 ((∀𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3433alanimi 1892 . . . . 5 ((∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3514, 30, 34syl2an 575 . . . 4 ((𝐴 = 𝐵𝐶 = 𝐷) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
36 eqeq2 2782 . . . . . . 7 (𝐸 = 𝐹 → (𝑧 = 𝐸𝑧 = 𝐹))
3736alrimiv 2007 . . . . . 6 (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹))
38372ralimi 3102 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
39 hbra1 3091 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
40 rsp 3078 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4139, 40alrimih 1899 . . . . . . . 8 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
42 19.21v 2020 . . . . . . . . 9 (∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4342albii 1895 . . . . . . . 8 (∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4441, 43sylibr 224 . . . . . . 7 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
4544ralimi 3101 . . . . . 6 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
46 hbra1 3091 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
47 rsp 3078 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
4846, 47alrimih 1899 . . . . . 6 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
49 19.21v 2020 . . . . . . . 8 (∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
50492albii 1896 . . . . . . 7 (∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
51719.21 2231 . . . . . . . 8 (∀𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5251albii 1895 . . . . . . 7 (∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5350, 52sylbbr 226 . . . . . 6 (∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5445, 48, 533syl 18 . . . . 5 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5538, 54syl 17 . . . 4 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
56 id 22 . . . . . . 7 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5756alanimi 1892 . . . . . 6 ((∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5857alanimi 1892 . . . . 5 ((∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5958alanimi 1892 . . . 4 ((∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
6035, 55, 59syl2an 575 . . 3 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
61 tsan2 34281 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦𝐶)))
6261ord 843 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦𝐶)))
63 tsan2 34281 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
6463a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
6562, 64cnf1dd 34224 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
66 tsbi2 34273 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6766ord 843 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6867a1dd 50 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
69 ax-1 6 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
7068, 69contrd 34231 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
7170a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
7265, 71cnf1dd 34224 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
73 idd 24 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐴))
74 tsan2 34281 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
7574ord 843 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
76 tsan2 34281 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
7776a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
7875, 77cnf1dd 34224 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
79 tsim2 34270 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8079a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
8178, 80cnf1dd 34224 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
82 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8381, 82contrd 34231 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴𝑥𝐵))
8483a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
85 tsbi3 34274 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8685a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8784, 86cnfn2dd 34227 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
8873, 87cnf1dd 34224 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
89 tsan2 34281 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷)))
9089a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷))))
9188, 90cnf1dd 34224 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦𝐷)))
92 tsan2 34281 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9392a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
9491, 93cnf1dd 34224 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9572, 94contrd 34231 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → 𝑥𝐴)
9695a1d 25 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐴))
97 ax-1 6 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
9879a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
9997, 98cnf2dd 34225 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
100 tsan3 34282 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
101100a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
10299, 101cnfn2dd 34227 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
10396, 102mpdd 43 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
104 notnotr 128 . . . . . . . . . . . . . . . . . 18 (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
105104a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
10692a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
107105, 106cnfn2dd 34227 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐵𝑦𝐷)))
108 tsan3 34282 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷)))
109108a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷))))
110107, 109cnfn2dd 34227 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐷))
111 tsan3 34282 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦𝐶𝑦𝐷) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
112111ord 843 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
11376a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
114112, 113cnf1dd 34224 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
11579a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
116114, 115cnf1dd 34224 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
117 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
118116, 117contrd 34231 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶𝑦𝐷))
119110, 118sylibrd 249 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐶))
12095a1d 25 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑥𝐴))
121 ax-1 6 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
12279a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
123121, 122cnf2dd 34225 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
124100a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
125123, 124cnfn2dd 34227 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
126120, 125mpdd 43 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
127119, 126mpdd 43 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸𝑧 = 𝐹)))
128120, 119jcad 496 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴𝑦𝐶)))
129 tsim3 34271 . . . . . . . . . . . . . . . . . . . 20 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
130129a1d 25 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
131121, 130cnf2dd 34225 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
132 tsbi1 34272 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
133132a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
134131, 133cnf2dd 34225 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
135105, 134cnfn2dd 34227 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
136 tsan1 34280 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
137136a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
138135, 137cnf2dd 34225 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸)))
139128, 138cnfn1dd 34226 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
140 tsan3 34282 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
141140a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
142105, 141cnfn2dd 34227 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
143 tsbi3 34274 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
144143a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
145144or32dd 34228 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
146142, 145cnfn2dd 34227 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
147139, 146cnf1dd 34224 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
148127, 147contrd 34231 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
149148a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
150129a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
15197, 150cnf2dd 34225 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
15266a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
153151, 152cnf2dd 34225 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
154149, 153cnf2dd 34225 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
15563a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
156154, 155cnfn2dd 34227 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴𝑦𝐶)))
157 tsan3 34282 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶)))
158157a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶))))
159156, 158cnfn2dd 34227 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐶))
160 tsan3 34282 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
161160a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
162154, 161cnfn2dd 34227 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
16396, 83sylibd 229 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐵))
164159, 118sylibd 229 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐷))
165163, 164jcad 496 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐵𝑦𝐷)))
166 tsan1 34280 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
167166a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
168149, 167cnf2dd 34225 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹)))
169165, 168cnfn1dd 34226 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
170 tsbi4 34275 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
171170a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
172171or32dd 34228 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
173169, 172cnf2dd 34225 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
174162, 173cnfn1dd 34226 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
175 tsim1 34269 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
176175a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
177176or32dd 34228 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ (𝑧 = 𝐸𝑧 = 𝐹))))
178174, 177cnf2dd 34225 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
179159, 178cnfn1dd 34226 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
180103, 179contrd 34231 . . . . . 6 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
181180efald2 34209 . . . . 5 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
182181alimi 1887 . . . 4 (∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
1831822alimi 1888 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
184 oprabbi 34302 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
18560, 183, 1843syl 18 . 2 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
186 df-mpt2 6798 . 2 (𝑥𝐴, 𝑦𝐶𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)}
187 df-mpt2 6798 . 2 (𝑥𝐵, 𝑦𝐷𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)}
188185, 186, 1873eqtr4g 2830 1 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  wal 1629   = wceq 1631  wfal 1636  wcel 2145  wnfc 2900  wral 3061  {coprab 6794  cmpt2 6795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-oprab 6797  df-mpt2 6798
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator