Metamath Proof Explorer

Theorem mpobi123f

Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses mpobi123f.1 ⊢ Ⅎ 𝑥 𝐴
mpobi123f.2 ⊢ Ⅎ 𝑥 𝐵
mpobi123f.3 ⊢ Ⅎ 𝑦 𝐴
mpobi123f.4 ⊢ Ⅎ 𝑦 𝐵
mpobi123f.5 ⊢ Ⅎ 𝑦 𝐶
mpobi123f.6 ⊢ Ⅎ 𝑦 𝐷
mpobi123f.7 ⊢ Ⅎ 𝑥 𝐶
mpobi123f.8 ⊢ Ⅎ 𝑥 𝐷
Assertion mpobi123f ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ 𝐸 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 mpobi123f.1 ⊢ Ⅎ 𝑥 𝐴
2 mpobi123f.2 ⊢ Ⅎ 𝑥 𝐵
3 mpobi123f.3 ⊢ Ⅎ 𝑦 𝐴
4 mpobi123f.4 ⊢ Ⅎ 𝑦 𝐵
5 mpobi123f.5 ⊢ Ⅎ 𝑦 𝐶
6 mpobi123f.6 ⊢ Ⅎ 𝑦 𝐷
7 mpobi123f.7 ⊢ Ⅎ 𝑥 𝐶
8 mpobi123f.8 ⊢ Ⅎ 𝑥 𝐷
9 1 2 nfeq ⊢ Ⅎ 𝑥 𝐴 = 𝐵
10 eleq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
11 9 10 alrimi ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
12 3 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
13 4 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐵
14 12 13 nfbi ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
15 ax-5 ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
16 14 15 alrimi ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
17 11 16 sylg ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
18 5 6 nfeq ⊢ Ⅎ 𝑦 𝐶 = 𝐷
19 eleq2 ⊢ ( 𝐶 = 𝐷 → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
20 18 19 alrimi ⊢ ( 𝐶 = 𝐷 → ∀ 𝑦 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
21 ax-5 ⊢ ( ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
22 21 alimi ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
23 7 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
24 8 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷
25 23 24 nfbi ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 )
26 25 nfal ⊢ Ⅎ 𝑥 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 )
27 26 nfal ⊢ Ⅎ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 )
28 27 nf5ri ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
29 20 22 28 3syl ⊢ ( 𝐶 = 𝐷 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
30 id ⊢ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) )
31 30 alanimi ⊢ ( ( ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) → ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) )
32 31 alanimi ⊢ ( ( ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) )
33 32 alanimi ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) )
34 17 29 33 syl2an ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) )
35 eqeq2 ⊢ ( 𝐸 = 𝐹 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) )
36 35 alrimiv ⊢ ( 𝐸 = 𝐹 → ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) )
37 36 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) )
38 hbra1 ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ∀ 𝑦 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) )
39 rsp ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ( 𝑦 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
40 38 39 alrimih ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
41 19.21v ⊢ ( ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ↔ ( 𝑦 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
42 41 albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
43 40 42 sylibr ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
44 43 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
45 hbra1 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) → ∀ 𝑥 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
46 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
47 45 46 alrimih ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
48 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
49 48 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
50 12 19.21 ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
51 50 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
52 49 51 sylbbr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
53 37 44 47 52 4syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
54 id ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
55 54 alanimi ⊢ ( ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
56 55 alanimi ⊢ ( ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
57 56 alanimi ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
58 34 53 57 syl2an ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
59 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐴 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
60 59 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
61 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
62 61 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
63 60 62 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
64 tsbi2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
65 64 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
66 65 a1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
67 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
68 66 67 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
69 68 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
70 63 69 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
71 idd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴 ) )
72 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
73 72 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
74 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
75 74 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
76 73 75 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
77 tsim2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
78 77 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
79 76 78 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
80 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
81 79 80 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
82 81 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
83 tsbi3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ∨ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
84 83 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ∨ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) ) )
85 82 84 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ) )
86 71 85 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
87 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐵 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
88 87 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) ) )
89 86 88 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
90 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
91 90 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
92 89 91 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
93 70 92 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → 𝑥 ∈ 𝐴 )
94 93 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑥 ∈ 𝐴 ) )
95 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
96 77 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
97 95 96 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
98 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
99 98 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
100 97 99 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
101 94 100 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
102 notnotr ⊢ ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) )
103 102 a1i ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
104 90 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
105 103 104 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
106 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐷 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
107 106 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑦 ∈ 𝐷 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) ) )
108 105 107 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑦 ∈ 𝐷 ) )
109 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
110 109 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
111 74 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
112 110 111 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
113 77 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
114 112 113 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
115 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
116 114 115 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
117 108 116 sylibrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑦 ∈ 𝐶 ) )
118 93 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑥 ∈ 𝐴 ) )
119 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
120 77 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
121 119 120 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
122 98 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
123 121 122 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
124 118 123 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
125 117 124 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
126 118 117 jcad ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
127 tsim3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
128 127 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
129 119 128 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
130 tsbi1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
131 130 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
132 129 131 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
133 103 132 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
134 tsan1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
135 134 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
136 133 135 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ) )
137 126 136 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ 𝑧 = 𝐸 ) )
138 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑧 = 𝐹 ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
139 138 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐹 ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
140 103 139 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑧 = 𝐹 ) )
141 tsbi3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
142 141 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
143 142 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ 𝑧 = 𝐹 ) ) )
144 140 143 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
145 137 144 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
146 125 145 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) )
147 146 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
148 127 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
149 95 148 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
150 64 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
151 149 150 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
152 147 151 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
153 61 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
154 152 153 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
155 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
156 155 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) ) )
157 154 156 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑦 ∈ 𝐶 ) )
158 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑧 = 𝐸 ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
159 158 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑧 = 𝐸 ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
160 152 159 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑧 = 𝐸 ) )
161 94 81 sylibd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑥 ∈ 𝐵 ) )
162 157 116 sylibd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑦 ∈ 𝐷 ) )
163 161 162 jcad ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
164 tsan1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
165 164 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
166 147 165 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ) )
167 163 166 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ 𝑧 = 𝐹 ) )
168 tsbi4 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
169 168 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
170 169 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ 𝑧 = 𝐹 ) ) )
171 167 170 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
172 160 171 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
173 tsim1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
174 173 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
175 174 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
176 172 175 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
177 157 176 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
178 101 177 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ⊥ )
179 178 efald2 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
180 179 alimi ⊢ ( ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
181 180 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
182 oprabbi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) } )
183 58 181 182 3syl ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) } )
184 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ 𝐸 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) }
185 df-mpo ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ 𝐹 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) }
186 183 184 185 3eqtr4g ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ 𝐸 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ 𝐹 ) )