Step | Hyp | Ref
| Expression |
1 | | excom 2162 |
. . . . . 6
⊢
(∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) ↔ ∃𝑧∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
2 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 = 〈𝑎, 𝑧〉 |
3 | | cnvoprabOLD.x |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝜓 |
4 | 2, 3 | nfan 1902 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
5 | 4 | nfex 2318 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
6 | | nfv 1917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑤 = 〈𝑎, 𝑧〉 |
7 | | cnvoprabOLD.y |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝜓 |
8 | 6, 7 | nfan 1902 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
9 | 8 | nfex 2318 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) |
10 | | opex 5379 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 ∈ V |
11 | | opeq1 4804 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑥, 𝑦〉 → 〈𝑎, 𝑧〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
12 | 11 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝑤 = 〈𝑎, 𝑧〉 ↔ 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
13 | | cnvoprabOLD.1 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜑)) |
14 | 12, 13 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑥, 𝑦〉 → ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) ↔ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
15 | 10, 14 | spcev 3545 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
16 | 9, 15 | exlimi 2210 |
. . . . . . . . 9
⊢
(∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
17 | 5, 16 | exlimi 2210 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
18 | | cnvoprabOLD.2 |
. . . . . . . . . . 11
⊢ (𝜓 → 𝑎 ∈ (V × V)) |
19 | 18 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → 𝑎 ∈ (V × V)) |
20 | | fvex 6787 |
. . . . . . . . . . 11
⊢
(1st ‘𝑎) ∈ V |
21 | | fvex 6787 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑎) ∈ V |
22 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑎) = 𝑥 ↔ 𝑥 = (1st ‘𝑎)) |
23 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑎) = 𝑦 ↔ 𝑦 = (2nd ‘𝑎)) |
24 | 22, 23 | anbi12i 627 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑎) = 𝑥 ∧ (2nd ‘𝑎) = 𝑦) ↔ (𝑥 = (1st ‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) |
25 | | eqopi 7867 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (V × V) ∧
((1st ‘𝑎)
= 𝑥 ∧ (2nd
‘𝑎) = 𝑦)) → 𝑎 = 〈𝑥, 𝑦〉) |
26 | 24, 25 | sylan2br 595 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (V × V) ∧
(𝑥 = (1st
‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) → 𝑎 = 〈𝑥, 𝑦〉) |
27 | 14 | bicomd 222 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑥, 𝑦〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (V × V) ∧
(𝑥 = (1st
‘𝑎) ∧ 𝑦 = (2nd ‘𝑎))) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓))) |
29 | 4, 8, 28 | spc2ed 3540 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (V × V) ∧
((1st ‘𝑎)
∈ V ∧ (2nd ‘𝑎) ∈ V)) → ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
30 | 20, 21, 29 | mpanr12 702 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (V × V) →
((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
31 | 19, 30 | mpcom 38 |
. . . . . . . . 9
⊢ ((𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
32 | 31 | exlimiv 1933 |
. . . . . . . 8
⊢
(∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓) → ∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
33 | 17, 32 | impbii 208 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
34 | 33 | exbii 1850 |
. . . . . 6
⊢
(∃𝑧∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧∃𝑎(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
35 | | exrot3 2165 |
. . . . . 6
⊢
(∃𝑧∃𝑥∃𝑦(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
36 | 1, 34, 35 | 3bitr2ri 300 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)) |
37 | 36 | abbii 2808 |
. . . 4
⊢ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} = {𝑤 ∣ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)} |
38 | | df-oprab 7279 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
39 | | df-opab 5137 |
. . . 4
⊢
{〈𝑎, 𝑧〉 ∣ 𝜓} = {𝑤 ∣ ∃𝑎∃𝑧(𝑤 = 〈𝑎, 𝑧〉 ∧ 𝜓)} |
40 | 37, 38, 39 | 3eqtr4ri 2777 |
. . 3
⊢
{〈𝑎, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
41 | 40 | cnveqi 5783 |
. 2
⊢ ◡{〈𝑎, 𝑧〉 ∣ 𝜓} = ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
42 | | cnvopab 6042 |
. 2
⊢ ◡{〈𝑎, 𝑧〉 ∣ 𝜓} = {〈𝑧, 𝑎〉 ∣ 𝜓} |
43 | 41, 42 | eqtr3i 2768 |
1
⊢ ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑧, 𝑎〉 ∣ 𝜓} |