Step | Hyp | Ref
| Expression |
1 | | excom 1657 |
. . . . . 6
⊢
(∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) ↔ ∃𝑧∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
2 | | nfv 1521 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 = 〈𝑎, 𝑧〉 |
3 | | cnvoprab.x |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝜓 |
4 | 2, 3 | nfan 1558 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
5 | 4 | nfex 1630 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
6 | | nfv 1521 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑤 = 〈𝑎, 𝑧〉 |
7 | | cnvoprab.y |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝜓 |
8 | 6, 7 | nfan 1558 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
9 | 8 | nfex 1630 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
10 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
11 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
12 | 10, 11 | opex 4212 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 ∈ V |
13 | | opeq1 3763 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑥, 𝑦〉 → 〈𝑎, 𝑧〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
14 | 13 | eqeq2d 2182 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝑤 = 〈𝑎, 𝑧〉 ↔ 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
15 | | cnvoprab.1 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜑)) |
16 | 14, 15 | anbi12d 470 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑥, 𝑦〉 → ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) ↔ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
17 | 12, 16 | spcev 2825 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
18 | 9, 17 | exlimi 1587 |
. . . . . . . . 9
⊢
(∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
19 | 5, 18 | exlimi 1587 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
20 | | cnvoprab.2 |
. . . . . . . . . . 11
⊢ (𝜓 → 𝑎 ∈ (V × V)) |
21 | 20 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → 𝑎 ∈ (V × V)) |
22 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
23 | | 1stexg 6143 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ V → (1st
‘𝑎) ∈
V) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1st ‘𝑎) ∈ V |
25 | | 2ndexg 6144 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ V → (2nd
‘𝑎) ∈
V) |
26 | 22, 25 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑎) ∈ V |
27 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑎) = 𝑥 ↔ 𝑥 = (1st ‘𝑎)) |
28 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑎) = 𝑦 ↔ 𝑦 = (2nd ‘𝑎)) |
29 | 27, 28 | anbi12i 457 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑎) = 𝑥 ∧ (2nd ‘𝑎) = 𝑦) ↔ (𝑥 = (1st ‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) |
30 | | eqopi 6148 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (V × V) ∧
((1st ‘𝑎)
= 𝑥 ∧ (2nd
‘𝑎) = 𝑦)) → 𝑎 = 〈𝑥, 𝑦〉) |
31 | 29, 30 | sylan2br 286 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (V × V) ∧
(𝑥 = (1st
‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) → 𝑎 = 〈𝑥, 𝑦〉) |
32 | 16 | bicomd 140 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑥, 𝑦〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓))) |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (V × V) ∧
(𝑥 = (1st
‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓))) |
34 | 4, 8, 33 | spc2ed 6209 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (V × V) ∧
((1st ‘𝑎)
∈ V ∧ (2nd ‘𝑎) ∈ V)) → ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
35 | 24, 26, 34 | mpanr12 437 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (V × V) →
((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
36 | 21, 35 | mpcom 36 |
. . . . . . . . 9
⊢ ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
37 | 36 | exlimiv 1591 |
. . . . . . . 8
⊢
(∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
38 | 19, 37 | impbii 125 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
39 | 38 | exbii 1598 |
. . . . . 6
⊢
(∃𝑧∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
40 | | exrot3 1683 |
. . . . . 6
⊢
(∃𝑧∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
41 | 1, 39, 40 | 3bitr2ri 208 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
42 | 41 | abbii 2286 |
. . . 4
⊢ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} = {𝑤 ∣ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)} |
43 | | df-oprab 5854 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
44 | | df-opab 4049 |
. . . 4
⊢
{〈𝑎, 𝑧〉 ∣ 𝜓} = {𝑤 ∣ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)} |
45 | 42, 43, 44 | 3eqtr4ri 2202 |
. . 3
⊢
{〈𝑎, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
46 | 45 | cnveqi 4784 |
. 2
⊢ ◡{〈𝑎, 𝑧〉 ∣ 𝜓} = ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
47 | | cnvopab 5010 |
. 2
⊢ ◡{〈𝑎, 𝑧〉 ∣ 𝜓} = {〈𝑧, 𝑎〉 ∣ 𝜓} |
48 | 46, 47 | eqtr3i 2193 |
1
⊢ ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑧, 𝑎〉 ∣ 𝜓} |