Step | Hyp | Ref
| Expression |
1 | | opex 5422 |
. 2
⊢
⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V |
2 | | opex 5422 |
. . . . . 6
⊢
⟨𝑥, 𝑦⟩ ∈ V |
3 | | vex 3450 |
. . . . . 6
⊢ 𝑧 ∈ V |
4 | 2, 3 | eqvinop 5445 |
. . . . 5
⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) |
5 | 4 | biimpi 215 |
. . . 4
⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) |
6 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) |
7 | | vex 3450 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
8 | | vex 3450 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
9 | 7, 8 | opth1 5433 |
. . . . . . . 8
⊢
(⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩) |
10 | 6, 9 | syl6bi 253 |
. . . . . . 7
⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)) |
11 | | vex 3450 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | | vex 3450 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
13 | 11, 12 | eqvinop 5445 |
. . . . . . . . 9
⊢ (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩)) |
14 | | opeq1 4831 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩) |
15 | 14 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)) |
16 | 11, 12, 3 | otth2 5441 |
. . . . . . . . . . . . . . 15
⊢
(⟨⟨𝑥,
𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡)) |
17 | | euequ 2596 |
. . . . . . . . . . . . . . . . . 18
⊢
∃!𝑥 𝑥 = 𝑟 |
18 | | eupick 2634 |
. . . . . . . . . . . . . . . . . 18
⊢
((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
19 | 17, 18 | mpan 689 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
20 | | euequ 2596 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑦 𝑦 = 𝑠 |
21 | | eupick 2634 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
22 | 20, 21 | mpan 689 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
23 | | euequ 2596 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑧 𝑧 = 𝑡 |
24 | | eupick 2634 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑧 = 𝑡 → 𝜑)) |
25 | 23, 24 | mpan 689 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑧(𝑧 = 𝑡 ∧ 𝜑) → (𝑧 = 𝑡 → 𝜑)) |
26 | 22, 25 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑))) |
27 | 19, 26 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑)))) |
28 | 27 | 3impd 1349 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) → 𝜑)) |
29 | 16, 28 | biimtrid 241 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑)) |
30 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
31 | 16, 30 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢
(⟨⟨𝑥,
𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
32 | 31 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
⊢
((⟨⟨𝑥,
𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑)) |
33 | | anass 470 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
34 | | anass 470 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
35 | 32, 33, 34 | 3bitri 297 |
. . . . . . . . . . . . . . . 16
⊢
((⟨⟨𝑥,
𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
36 | 35 | 3exbii 1853 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
37 | | nfe1 2148 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
38 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
39 | 38 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
40 | 39 | eximi 1838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑧(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
41 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
42 | 41 | drex1v 2368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑧(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
43 | 40, 42 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
44 | | 19.40 1890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (∃𝑧 𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
45 | | nfvd 1919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟) |
46 | 45 | 19.9d 2197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∃𝑧 𝑥 = 𝑟 → 𝑥 = 𝑟)) |
47 | 46 | anim1d 612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ((∃𝑧 𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
48 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
49 | 44, 47, 48 | syl56 36 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
50 | 43, 49 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
51 | 37, 50 | exlimi 2211 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
52 | 51 | eximi 1838 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
53 | | excom 2163 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
54 | | excom 2163 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
55 | 52, 53, 54 | 3imtr4i 292 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
56 | | nfe1 2148 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
57 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
58 | 57 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
59 | 58 | eximi 1838 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
60 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
61 | 60 | drex1v 2368 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
62 | 59, 61 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
63 | | 19.40 1890 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (∃𝑦 𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
64 | | nfvd 1919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟) |
65 | 64 | 19.9d 2197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑦 𝑥 = 𝑟 → 𝑥 = 𝑟)) |
66 | 65 | anim1d 612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ((∃𝑦 𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
67 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
68 | 63, 66, 67 | syl56 36 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))) |
69 | 62, 68 | pm2.61i 182 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
70 | 56, 69 | exlimi 2211 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
71 | | nfe1 2148 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) |
72 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 = 𝑡 ∧ 𝜑) → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) |
73 | 72 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
74 | 73 | eximi 1838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑧(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
75 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 𝑦 = 𝑧 → ((𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
76 | 75 | drex1v 2368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 𝑦 = 𝑧 → (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) ↔ ∃𝑧(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
77 | 74, 76 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑦 𝑦 = 𝑧 → (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
78 | | 19.40 1890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → (∃𝑧 𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
79 | | nfvd 1919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠) |
80 | 79 | 19.9d 2197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑧 𝑦 = 𝑠 → 𝑦 = 𝑠)) |
81 | 80 | anim1d 612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ((∃𝑧 𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
82 | | 19.8a 2175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
83 | 78, 81, 82 | syl56 36 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
84 | 77, 83 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
85 | 71, 84 | exlimi 2211 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
86 | 85 | anim2i 618 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
87 | 86 | eximi 1838 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
88 | 55, 70, 87 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
89 | 36, 88 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
90 | 29, 89 | syl11 33 |
. . . . . . . . . . . . 13
⊢
(⟨⟨𝑥,
𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)) |
91 | | eqeq1 2741 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) |
92 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢
(⟨⟨𝑟,
𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩) |
93 | 91, 92 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)) |
94 | 93 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑))) |
95 | 94 | 3exbidv 1929 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑))) |
96 | 95 | imbi1d 342 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))) |
97 | 93, 96 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))) |
98 | 90, 97 | mpbiri 258 |
. . . . . . . . . . . 12
⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))) |
99 | 15, 98 | syl6bi 253 |
. . . . . . . . . . 11
⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))) |
100 | 99 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))) |
101 | 100 | exlimivv 1936 |
. . . . . . . . 9
⊢
(∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))) |
102 | 13, 101 | sylbi 216 |
. . . . . . . 8
⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))) |
103 | 102 | com3l 89 |
. . . . . . 7
⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))) |
104 | 10, 103 | mpdd 43 |
. . . . . 6
⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))) |
105 | 104 | adantr 482 |
. . . . 5
⊢ ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))) |
106 | 105 | exlimivv 1936 |
. . . 4
⊢
(∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))) |
107 | 5, 106 | mpcom 38 |
. . 3
⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) |
108 | | 19.8a 2175 |
. . . . 5
⊢ ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)) |
109 | | 19.8a 2175 |
. . . . 5
⊢
(∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)) |
110 | | 19.8a 2175 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)) |
111 | 108, 109,
110 | 3syl 18 |
. . . 4
⊢ ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)) |
112 | 111 | ex 414 |
. . 3
⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))) |
113 | 107, 112 | impbid 211 |
. 2
⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑)) |
114 | | df-oprab 7362 |
. 2
⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} |
115 | 1, 113, 114 | elab2 3635 |
1
⊢
(⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑) |