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 44 47 52 3syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
54 37 53 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
55 id ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
56 55 alanimi ⊢ ( ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
57 56 alanimi ⊢ ( ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
58 57 alanimi ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
59 34 54 58 syl2an ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
60 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐴 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
61 60 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
62 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
63 62 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
64 61 63 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
65 tsbi2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
66 65 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
67 66 a1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
68 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
69 67 68 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
70 69 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
71 64 70 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
72 idd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴 ) )
73 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
74 73 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
75 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
76 75 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
77 74 76 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
78 tsim2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
79 78 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
80 77 79 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
81 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
82 80 81 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
83 82 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
84 tsbi3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ∨ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
85 84 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ∨ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) ) )
86 83 85 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵 ) ) )
87 72 86 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
88 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑥 ∈ 𝐵 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
89 88 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) ) )
90 87 89 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
91 tsan2 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
92 91 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
93 90 92 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
94 71 93 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → 𝑥 ∈ 𝐴 )
95 94 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑥 ∈ 𝐴 ) )
96 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
97 78 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
98 96 97 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
99 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
100 99 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
101 98 100 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
102 95 101 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
103 notnotr ⊢ ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) )
104 103 a1i ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
105 91 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
106 104 105 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
107 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐷 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
108 107 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑦 ∈ 𝐷 ∨ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) ) )
109 106 108 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑦 ∈ 𝐷 ) )
110 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
111 110 ord ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ) )
112 75 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
113 111 112 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
114 78 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
115 113 114 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
116 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
117 115 116 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
118 109 117 sylibrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑦 ∈ 𝐶 ) )
119 94 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑥 ∈ 𝐴 ) )
120 ax-1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
121 78 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
122 120 121 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) )
123 99 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ¬ ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) ) ) )
124 122 123 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
125 119 124 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
126 118 125 mpdd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
127 119 118 jcad ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
128 tsim3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
129 128 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
130 120 129 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
131 tsbi1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
132 131 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
133 130 132 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
134 104 133 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
135 tsan1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
136 135 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
137 134 136 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ 𝑧 = 𝐸 ) ) )
138 127 137 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ 𝑧 = 𝐸 ) )
139 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑧 = 𝐹 ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
140 139 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐹 ∨ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
141 104 140 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → 𝑧 = 𝐹 ) )
142 tsbi3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( 𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
143 142 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
144 143 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ 𝑧 = 𝐹 ) ) )
145 141 144 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ( 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
146 138 145 cnf1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) → ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
147 126 146 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) )
148 147 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
149 128 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) ) )
150 96 149 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
151 65 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ∨ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) ) )
152 150 151 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
153 148 152 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
154 62 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
155 153 154 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
156 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
157 156 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) ) )
158 155 157 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑦 ∈ 𝐶 ) )
159 tsan3 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( 𝑧 = 𝐸 ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) )
160 159 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑧 = 𝐸 ∨ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ) ) )
161 153 160 cnfn2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑧 = 𝐸 ) )
162 95 82 sylibd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑥 ∈ 𝐵 ) )
163 158 117 sylibd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → 𝑦 ∈ 𝐷 ) )
164 162 163 jcad ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ) )
165 tsan1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
166 165 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) )
167 148 166 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∨ ¬ 𝑧 = 𝐹 ) ) )
168 164 167 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ 𝑧 = 𝐹 ) )
169 tsbi4 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
170 169 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹 ) ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
171 170 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ 𝑧 = 𝐹 ) ) )
172 168 171 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ 𝑧 = 𝐸 ∨ ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
173 161 172 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) )
174 tsim1 ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
175 174 a1d ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
176 175 or32dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ∨ ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
177 173 176 cnf2dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ( ¬ 𝑦 ∈ 𝐶 ∨ ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) )
178 158 177 cnfn1dd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) )
179 102 178 contrd ⊢ ( ¬ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) ) → ⊥ )
180 179 efald2 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
181 180 alimi ⊢ ( ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
182 181 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → ( 𝑧 = 𝐸 ↔ 𝑧 = 𝐹 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) )
183 oprabbi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) } )
184 59 182 183 3syl ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) } )
185 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ 𝐸 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 = 𝐸 ) }
186 df-mpo ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ 𝐹 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 = 𝐹 ) }
187 184 185 186 3eqtr4g ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝐸 = 𝐹 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ 𝐸 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ 𝐹 ) )