Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . 4
⊢ x ∈
V |
2 | | vex 2554 |
. . . 4
⊢ y ∈
V |
3 | 1, 2 | opex 3957 |
. . 3
⊢
〈x, y〉 ∈
V |
4 | | vex 2554 |
. . 3
⊢ z ∈
V |
5 | | opexg 3955 |
. . 3
⊢
((〈x, y〉 ∈ V ∧ z ∈ V) → 〈〈x, y〉,
z〉 ∈
V) |
6 | 3, 4, 5 | mp2an 402 |
. 2
⊢
〈〈x, y〉, z〉
∈ V |
7 | 3, 4 | eqvinop 3971 |
. . . . 5
⊢ (w = 〈〈x, y〉,
z〉 ↔ ∃𝑎∃𝑡(w = 〈𝑎, 𝑡〉 ∧
〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉)) |
8 | 7 | biimpi 113 |
. . . 4
⊢ (w = 〈〈x, y〉,
z〉 → ∃𝑎∃𝑡(w = 〈𝑎, 𝑡〉 ∧
〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉)) |
9 | | eqeq1 2043 |
. . . . . . . 8
⊢ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 ↔ 〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉)) |
10 | | vex 2554 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
11 | | vex 2554 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
12 | 10, 11 | opth1 3964 |
. . . . . . . 8
⊢
(〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉 → 𝑎 = 〈x, y〉) |
13 | 9, 12 | syl6bi 152 |
. . . . . . 7
⊢ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → 𝑎 = 〈x, y〉)) |
14 | 1, 2 | eqvinop 3971 |
. . . . . . . . 9
⊢ (𝑎 = 〈x, y〉
↔ ∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧
〈𝑟, 𝑠〉 = 〈x, y〉)) |
15 | | opeq1 3540 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑟, 𝑠〉 → 〈𝑎, 𝑡〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
16 | 15 | eqeq2d 2048 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (w = 〈𝑎, 𝑡〉 ↔ w = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
17 | 1, 2, 4 | otth2 3969 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ (x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡)) |
18 | | df-3an 886 |
. . . . . . . . . . . . . . . . . . 19
⊢
((x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡)) |
19 | 17, 18 | bitri 173 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡)) |
20 | 19 | anbi1i 431 |
. . . . . . . . . . . . . . . . 17
⊢
((〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) ↔ (((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ)) |
21 | | anass 381 |
. . . . . . . . . . . . . . . . 17
⊢
((((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧
(z = 𝑡 ∧ φ))) |
22 | | anass 381 |
. . . . . . . . . . . . . . . . 17
⊢
(((x = 𝑟 ∧ y = 𝑠) ∧
(z = 𝑡 ∧ φ)) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
23 | 20, 21, 22 | 3bitri 195 |
. . . . . . . . . . . . . . . 16
⊢
((〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
24 | 23 | 3exbii 1495 |
. . . . . . . . . . . . . . 15
⊢ (∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) ↔ ∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
25 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
26 | 25 | eximi 1488 |
. . . . . . . . . . . . . . . . 17
⊢ (∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃y∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
27 | | excom 1551 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) ↔ ∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
28 | | excom 1551 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) ↔ ∃y∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
29 | 26, 27, 28 | 3imtr4i 190 |
. . . . . . . . . . . . . . . 16
⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
30 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . 16
⊢ (∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)))) |
31 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)) → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) |
32 | 31 | anim2i 324 |
. . . . . . . . . . . . . . . . 17
⊢
((x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → (x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
33 | 32 | eximi 1488 |
. . . . . . . . . . . . . . . 16
⊢ (∃x(x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
34 | 29, 30, 33 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
35 | 24, 34 | sylbi 114 |
. . . . . . . . . . . . . 14
⊢ (∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
36 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∃!x x = 𝑟 |
37 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((∃!x x = 𝑟 ∧ ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
38 | 36, 37 | mpan 400 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) |
39 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∃!y y = 𝑠 |
40 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∃!y y = 𝑠 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ))) |
41 | 39, 40 | mpan 400 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ))) |
42 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∃!z z = 𝑡 |
43 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∃!z z = 𝑡 ∧ ∃z(z = 𝑡 ∧ φ)) → (z = 𝑡 → φ)) |
44 | 42, 43 | mpan 400 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃z(z = 𝑡 ∧ φ) → (z = 𝑡 → φ)) |
45 | 41, 44 | syl6 29 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)) → (y = 𝑠 → (z = 𝑡 → φ))) |
46 | 38, 45 | syl6 29 |
. . . . . . . . . . . . . . . . 17
⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (x = 𝑟 → (y = 𝑠 → (z = 𝑡 → φ)))) |
47 | 46 | 3impd 1117 |
. . . . . . . . . . . . . . . 16
⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → ((x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡) → φ)) |
48 | 17, 47 | syl5bi 141 |
. . . . . . . . . . . . . . 15
⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (〈〈x, y〉,
z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → φ)) |
49 | 48 | com12 27 |
. . . . . . . . . . . . . 14
⊢
(〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → φ)) |
50 | 35, 49 | syl5 28 |
. . . . . . . . . . . . 13
⊢
(〈〈x, y〉, z〉
= 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) → φ)) |
51 | | eqeq1 2043 |
. . . . . . . . . . . . . . 15
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → (w = 〈〈x, y〉,
z〉 ↔ 〈〈𝑟, 𝑠〉, 𝑡〉 = 〈〈x, y〉,
z〉)) |
52 | | eqcom 2039 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑟, 𝑠〉, 𝑡〉 = 〈〈x, y〉,
z〉 ↔ 〈〈x, y〉,
z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
53 | 51, 52 | syl6bb 185 |
. . . . . . . . . . . . . 14
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → (w = 〈〈x, y〉,
z〉 ↔ 〈〈x, y〉,
z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
54 | 53 | anbi1d 438 |
. . . . . . . . . . . . . . . 16
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((w = 〈〈x, y〉,
z〉 ∧
φ) ↔ (〈〈x, y〉,
z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ))) |
55 | 54 | 3exbidv 1746 |
. . . . . . . . . . . . . . 15
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) ↔ ∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ))) |
56 | 55 | imbi1d 220 |
. . . . . . . . . . . . . 14
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ) ↔ (∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) → φ))) |
57 | 53, 56 | imbi12d 223 |
. . . . . . . . . . . . 13
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)) ↔ (〈〈x, y〉,
z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃x∃y∃z(〈〈x,
y〉, z〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧
φ) → φ)))) |
58 | 50, 57 | mpbiri 157 |
. . . . . . . . . . . 12
⊢ (w = 〈〈𝑟, 𝑠〉, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ))) |
59 | 16, 58 | syl6bi 152 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)))) |
60 | 59 | adantr 261 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈𝑟, 𝑠〉 ∧
〈𝑟, 𝑠〉 = 〈x, y〉)
→ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)))) |
61 | 60 | exlimivv 1773 |
. . . . . . . . 9
⊢ (∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧
〈𝑟, 𝑠〉 = 〈x, y〉)
→ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)))) |
62 | 14, 61 | sylbi 114 |
. . . . . . . 8
⊢ (𝑎 = 〈x, y〉
→ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)))) |
63 | 62 | com3l 75 |
. . . . . . 7
⊢ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (𝑎 = 〈x, y〉
→ (∃x∃y∃z(w =
〈〈x, y〉, z〉
∧ φ)
→ φ)))) |
64 | 13, 63 | mpdd 36 |
. . . . . 6
⊢ (w = 〈𝑎, 𝑡〉 → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ))) |
65 | 64 | adantr 261 |
. . . . 5
⊢
((w = 〈𝑎, 𝑡〉 ∧
〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉) → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ))) |
66 | 65 | exlimivv 1773 |
. . . 4
⊢ (∃𝑎∃𝑡(w = 〈𝑎, 𝑡〉 ∧
〈𝑎, 𝑡〉 = 〈〈x, y〉,
z〉) → (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ))) |
67 | 8, 66 | mpcom 32 |
. . 3
⊢ (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → φ)) |
68 | | 19.8a 1479 |
. . . . 5
⊢
((w = 〈〈x, y〉,
z〉 ∧
φ) → ∃z(w = 〈〈x, y〉,
z〉 ∧
φ)) |
69 | | 19.8a 1479 |
. . . . 5
⊢ (∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → ∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ)) |
70 | | 19.8a 1479 |
. . . . 5
⊢ (∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) → ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ)) |
71 | 68, 69, 70 | 3syl 17 |
. . . 4
⊢
((w = 〈〈x, y〉,
z〉 ∧
φ) → ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ)) |
72 | 71 | ex 108 |
. . 3
⊢ (w = 〈〈x, y〉,
z〉 → (φ → ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ))) |
73 | 67, 72 | impbid 120 |
. 2
⊢ (w = 〈〈x, y〉,
z〉 → (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ) ↔ φ)) |
74 | | df-oprab 5459 |
. 2
⊢
{〈〈x, y〉, z〉
∣ φ} = {w ∣ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
φ)} |
75 | 6, 73, 74 | elab2 2684 |
1
⊢
(〈〈x, y〉, z〉
∈ {〈〈x, y〉,
z〉 ∣ φ} ↔ φ) |