Step | Hyp | Ref
| Expression |
1 | | vex 2863 |
. . . 4
⊢ x ∈
V |
2 | | vex 2863 |
. . . 4
⊢ y ∈
V |
3 | 1, 2 | opex 4589 |
. . 3
⊢ ⟨x, y⟩ ∈ V |
4 | | vex 2863 |
. . 3
⊢ z ∈
V |
5 | 3, 4 | opex 4589 |
. 2
⊢ ⟨⟨x, y⟩, z⟩ ∈
V |
6 | 3, 4 | eqvinop 4607 |
. . . . 5
⊢ (w = ⟨⟨x, y⟩, z⟩ ↔ ∃a∃t(w = ⟨a, t⟩ ∧ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)) |
7 | 6 | biimpi 186 |
. . . 4
⊢ (w = ⟨⟨x, y⟩, z⟩ → ∃a∃t(w = ⟨a, t⟩ ∧ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)) |
8 | | eqeq1 2359 |
. . . . . . . 8
⊢ (w = ⟨a, t⟩ → (w =
⟨⟨x, y⟩, z⟩ ↔ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)) |
9 | | opth 4603 |
. . . . . . . . 9
⊢ (⟨a, t⟩ = ⟨⟨x, y⟩, z⟩ ↔ (a =
⟨x,
y⟩ ∧ t = z)) |
10 | 9 | simplbi 446 |
. . . . . . . 8
⊢ (⟨a, t⟩ = ⟨⟨x, y⟩, z⟩ → a =
⟨x,
y⟩) |
11 | 8, 10 | syl6bi 219 |
. . . . . . 7
⊢ (w = ⟨a, t⟩ → (w =
⟨⟨x, y⟩, z⟩ → a =
⟨x,
y⟩)) |
12 | 1, 2 | eqvinop 4607 |
. . . . . . . . 9
⊢ (a = ⟨x, y⟩ ↔ ∃r∃s(a = ⟨r, s⟩ ∧ ⟨r, s⟩ = ⟨x, y⟩)) |
13 | | opeq1 4579 |
. . . . . . . . . . . . 13
⊢ (a = ⟨r, s⟩ → ⟨a, t⟩ = ⟨⟨r, s⟩, t⟩) |
14 | 13 | eqeq2d 2364 |
. . . . . . . . . . . 12
⊢ (a = ⟨r, s⟩ → (w =
⟨a,
t⟩ ↔
w = ⟨⟨r, s⟩, t⟩)) |
15 | | opth 4603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ↔ (⟨x, y⟩ = ⟨r, s⟩ ∧ z = t)) |
16 | | opth 4603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟨x, y⟩ = ⟨r, s⟩ ↔
(x = r
∧ y =
s)) |
17 | 16 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((⟨x, y⟩ = ⟨r, s⟩ ∧ z = t) ↔ ((x =
r ∧
y = s)
∧ z =
t)) |
18 | 15, 17 | bitri 240 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ↔
((x = r
∧ y =
s) ∧
z = t)) |
19 | 18 | anbi1i 676 |
. . . . . . . . . . . . . . . . 17
⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) ↔
(((x = r ∧ y = s) ∧ z = t) ∧ φ)) |
20 | | anass 630 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x = r ∧ y = s) ∧ z = t) ∧ φ) ↔
((x = r
∧ y =
s) ∧
(z = t
∧ φ))) |
21 | | anass 630 |
. . . . . . . . . . . . . . . . 17
⊢ (((x = r ∧ y = s) ∧ (z = t ∧ φ)) ↔
(x = r
∧ (y =
s ∧
(z = t
∧ φ)))) |
22 | 19, 20, 21 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) ↔
(x = r
∧ (y =
s ∧
(z = t
∧ φ)))) |
23 | 22 | 3exbii 1584 |
. . . . . . . . . . . . . . 15
⊢ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) ↔
∃x∃y∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))) |
24 | | nfcvf2 2513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬ ∀x x = z →
Ⅎzx) |
25 | | nfcvd 2491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬ ∀x x = z →
Ⅎzr) |
26 | 24, 25 | nfeqd 2504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ ∀x x = z →
Ⅎz x = r) |
27 | 26 | exdistrf 1971 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃x∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))
→ ∃x(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))) |
28 | 27 | eximi 1576 |
. . . . . . . . . . . . . . . . 17
⊢ (∃y∃x∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))
→ ∃y∃x(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))) |
29 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x∃y∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))
↔ ∃y∃x∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))) |
30 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x∃y(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))
↔ ∃y∃x(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))) |
31 | 28, 29, 30 | 3imtr4i 257 |
. . . . . . . . . . . . . . . 16
⊢ (∃x∃y∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))
→ ∃x∃y(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))) |
32 | | nfcvf2 2513 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬ ∀x x = y →
Ⅎyx) |
33 | | nfcvd 2491 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬ ∀x x = y →
Ⅎyr) |
34 | 32, 33 | nfeqd 2504 |
. . . . . . . . . . . . . . . . 17
⊢ (¬ ∀x x = y →
Ⅎy x = r) |
35 | 34 | exdistrf 1971 |
. . . . . . . . . . . . . . . 16
⊢ (∃x∃y(x = r ∧ ∃z(y = s ∧ (z = t ∧ φ)))
→ ∃x(x = r ∧ ∃y∃z(y = s ∧ (z = t ∧ φ)))) |
36 | | nfcvf2 2513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬ ∀y y = z →
Ⅎzy) |
37 | | nfcvd 2491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬ ∀y y = z →
Ⅎzs) |
38 | 36, 37 | nfeqd 2504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ ∀y y = z →
Ⅎz y = s) |
39 | 38 | exdistrf 1971 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃y∃z(y = s ∧ (z = t ∧ φ)) → ∃y(y = s ∧ ∃z(z = t ∧ φ))) |
40 | 39 | anim2i 552 |
. . . . . . . . . . . . . . . . 17
⊢ ((x = r ∧ ∃y∃z(y = s ∧ (z = t ∧ φ)))
→ (x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
41 | 40 | eximi 1576 |
. . . . . . . . . . . . . . . 16
⊢ (∃x(x = r ∧ ∃y∃z(y = s ∧ (z = t ∧ φ)))
→ ∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
42 | 31, 35, 41 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (∃x∃y∃z(x = r ∧ (y = s ∧ (z = t ∧ φ)))
→ ∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
43 | 23, 42 | sylbi 187 |
. . . . . . . . . . . . . 14
⊢ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) →
∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
44 | | df-3an 936 |
. . . . . . . . . . . . . . . . 17
⊢ ((x = r ∧ y = s ∧ z = t) ↔
((x = r
∧ y =
s) ∧
z = t)) |
45 | 18, 44 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ↔
(x = r
∧ y =
s ∧
z = t)) |
46 | | euequ1 2292 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∃!x x = r |
47 | | eupick 2267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((∃!x x = r ∧ ∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))) → (x = r →
∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
48 | 46, 47 | mpan 651 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ (x = r → ∃y(y = s ∧ ∃z(z = t ∧ φ)))) |
49 | | euequ1 2292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∃!y y = s |
50 | | eupick 2267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∃!y y = s ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ (y = s → ∃z(z = t ∧ φ))) |
51 | 49, 50 | mpan 651 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃y(y = s ∧ ∃z(z = t ∧ φ)) → (y = s →
∃z(z = t ∧ φ))) |
52 | | euequ1 2292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∃!z z = t |
53 | | eupick 2267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∃!z z = t ∧ ∃z(z = t ∧ φ)) → (z = t →
φ)) |
54 | 52, 53 | mpan 651 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃z(z = t ∧ φ) →
(z = t
→ φ)) |
55 | 51, 54 | syl6 29 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃y(y = s ∧ ∃z(z = t ∧ φ)) → (y = s →
(z = t
→ φ))) |
56 | 48, 55 | syl6 29 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ (x = r → (y =
s → (z = t →
φ)))) |
57 | 56 | 3impd 1165 |
. . . . . . . . . . . . . . . 16
⊢ (∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ ((x = r ∧ y = s ∧ z = t) → φ)) |
58 | 45, 57 | syl5bi 208 |
. . . . . . . . . . . . . . 15
⊢ (∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ → φ)) |
59 | 58 | com12 27 |
. . . . . . . . . . . . . 14
⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ → (∃x(x = r ∧ ∃y(y = s ∧ ∃z(z = t ∧ φ)))
→ φ)) |
60 | 43, 59 | syl5 28 |
. . . . . . . . . . . . 13
⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ → (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) →
φ)) |
61 | | eqeq1 2359 |
. . . . . . . . . . . . . . 15
⊢ (w = ⟨⟨r, s⟩, t⟩ →
(w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩)) |
62 | | eqcom 2355 |
. . . . . . . . . . . . . . 15
⊢ (⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩) |
63 | 61, 62 | syl6bb 252 |
. . . . . . . . . . . . . 14
⊢ (w = ⟨⟨r, s⟩, t⟩ →
(w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩)) |
64 | 63 | anbi1d 685 |
. . . . . . . . . . . . . . . 16
⊢ (w = ⟨⟨r, s⟩, t⟩ →
((w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ))) |
65 | 64 | 3exbidv 1629 |
. . . . . . . . . . . . . . 15
⊢ (w = ⟨⟨r, s⟩, t⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔
∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ))) |
66 | 65 | imbi1d 308 |
. . . . . . . . . . . . . 14
⊢ (w = ⟨⟨r, s⟩, t⟩ → ((∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ) ↔ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) →
φ))) |
67 | 63, 66 | imbi12d 311 |
. . . . . . . . . . . . 13
⊢ (w = ⟨⟨r, s⟩, t⟩ →
((w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)) ↔ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ → (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ ∧ φ) →
φ)))) |
68 | 60, 67 | mpbiri 224 |
. . . . . . . . . . . 12
⊢ (w = ⟨⟨r, s⟩, t⟩ →
(w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ))) |
69 | 14, 68 | syl6bi 219 |
. . . . . . . . . . 11
⊢ (a = ⟨r, s⟩ → (w =
⟨a,
t⟩ →
(w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)))) |
70 | 69 | adantr 451 |
. . . . . . . . . 10
⊢ ((a = ⟨r, s⟩ ∧ ⟨r, s⟩ = ⟨x, y⟩) →
(w = ⟨a, t⟩ →
(w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)))) |
71 | 70 | exlimivv 1635 |
. . . . . . . . 9
⊢ (∃r∃s(a = ⟨r, s⟩ ∧ ⟨r, s⟩ = ⟨x, y⟩) →
(w = ⟨a, t⟩ →
(w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)))) |
72 | 12, 71 | sylbi 187 |
. . . . . . . 8
⊢ (a = ⟨x, y⟩ → (w =
⟨a,
t⟩ →
(w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)))) |
73 | 72 | com3l 75 |
. . . . . . 7
⊢ (w = ⟨a, t⟩ → (w =
⟨⟨x, y⟩, z⟩ → (a =
⟨x,
y⟩ →
(∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)))) |
74 | 11, 73 | mpdd 36 |
. . . . . 6
⊢ (w = ⟨a, t⟩ → (w =
⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ))) |
75 | 74 | adantr 451 |
. . . . 5
⊢ ((w = ⟨a, t⟩ ∧ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) → (w =
⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ))) |
76 | 75 | exlimivv 1635 |
. . . 4
⊢ (∃a∃t(w = ⟨a, t⟩ ∧ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) → (w =
⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ))) |
77 | 7, 76 | mpcom 32 |
. . 3
⊢ (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
φ)) |
78 | | 19.8a 1756 |
. . . . 5
⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
79 | | 19.8a 1756 |
. . . . 5
⊢ (∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
80 | | 19.8a 1756 |
. . . . 5
⊢ (∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
81 | 78, 79, 80 | 3syl 18 |
. . . 4
⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) →
∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
82 | 81 | ex 423 |
. . 3
⊢ (w = ⟨⟨x, y⟩, z⟩ → (φ → ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))) |
83 | 77, 82 | impbid 183 |
. 2
⊢ (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔
φ)) |
84 | | df-oprab 5529 |
. 2
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w
∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)} |
85 | 5, 83, 84 | elab2 2989 |
1
⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ) |