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