Step | Hyp | Ref
| Expression |
1 | | excom 2163 |
. . . 4
⊢
(∃𝑦∃𝑝∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
2 | | opex 5426 |
. . . . . . . 8
⊢
⟨𝑧, 𝑦⟩ ∈ V |
3 | | breq1 5113 |
. . . . . . . . . 10
⊢ (𝑝 = ⟨𝑧, 𝑦⟩ → (𝑝1st 𝑥 ↔ ⟨𝑧, 𝑦⟩1st 𝑥)) |
4 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑝 = ⟨𝑧, 𝑦⟩ → (𝑝 ∈ 𝐴 ↔ ⟨𝑧, 𝑦⟩ ∈ 𝐴)) |
5 | 3, 4 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑝 = ⟨𝑧, 𝑦⟩ → ((𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴) ↔ (⟨𝑧, 𝑦⟩1st 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))) |
6 | | vex 3452 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
7 | | vex 3452 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
8 | 6, 7 | br1steq 34384 |
. . . . . . . . . . 11
⊢
(⟨𝑧, 𝑦⟩1st 𝑥 ↔ 𝑥 = 𝑧) |
9 | | equcom 2022 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
10 | 8, 9 | bitri 275 |
. . . . . . . . . 10
⊢
(⟨𝑧, 𝑦⟩1st 𝑥 ↔ 𝑧 = 𝑥) |
11 | 10 | anbi1i 625 |
. . . . . . . . 9
⊢
((⟨𝑧, 𝑦⟩1st 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (𝑧 = 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴)) |
12 | 5, 11 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑝 = ⟨𝑧, 𝑦⟩ → ((𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴) ↔ (𝑧 = 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))) |
13 | 2, 12 | ceqsexv 3497 |
. . . . . . 7
⊢
(∃𝑝(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ (𝑧 = 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴)) |
14 | 13 | exbii 1851 |
. . . . . 6
⊢
(∃𝑧∃𝑝(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴)) |
15 | | excom 2163 |
. . . . . 6
⊢
(∃𝑧∃𝑝(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑝∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
16 | | vex 3452 |
. . . . . . 7
⊢ 𝑥 ∈ V |
17 | | opeq1 4835 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ⟨𝑧, 𝑦⟩ = ⟨𝑥, 𝑦⟩) |
18 | 17 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (⟨𝑧, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)) |
19 | 16, 18 | ceqsexv 3497 |
. . . . . 6
⊢
(∃𝑧(𝑧 = 𝑥 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴) |
20 | 14, 15, 19 | 3bitr3ri 302 |
. . . . 5
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑝∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
21 | 20 | exbii 1851 |
. . . 4
⊢
(∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑦∃𝑝∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
22 | | ancom 462 |
. . . . . 6
⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ (𝑝(1st ↾ (V × V))𝑥 ∧ 𝑝 ∈ 𝐴)) |
23 | | anass 470 |
. . . . . . 7
⊢
(((∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ 𝑝1st 𝑥) ∧ 𝑝 ∈ 𝐴) ↔ (∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
24 | 16 | brresi 5951 |
. . . . . . . . 9
⊢ (𝑝(1st ↾ (V
× V))𝑥 ↔ (𝑝 ∈ (V × V) ∧
𝑝1st 𝑥)) |
25 | | elvv 5711 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (V × V) ↔
∃𝑧∃𝑦 𝑝 = ⟨𝑧, 𝑦⟩) |
26 | | excom 2163 |
. . . . . . . . . . 11
⊢
(∃𝑧∃𝑦 𝑝 = ⟨𝑧, 𝑦⟩ ↔ ∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩) |
27 | 25, 26 | bitri 275 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (V × V) ↔
∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩) |
28 | 27 | anbi1i 625 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (V × V) ∧
𝑝1st 𝑥) ↔ (∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ 𝑝1st 𝑥)) |
29 | 24, 28 | bitri 275 |
. . . . . . . 8
⊢ (𝑝(1st ↾ (V
× V))𝑥 ↔
(∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ 𝑝1st 𝑥)) |
30 | 29 | anbi1i 625 |
. . . . . . 7
⊢ ((𝑝(1st ↾ (V
× V))𝑥 ∧ 𝑝 ∈ 𝐴) ↔ ((∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ 𝑝1st 𝑥) ∧ 𝑝 ∈ 𝐴)) |
31 | | 19.41vv 1955 |
. . . . . . 7
⊢
(∃𝑦∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ (∃𝑦∃𝑧 𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
32 | 23, 30, 31 | 3bitr4i 303 |
. . . . . 6
⊢ ((𝑝(1st ↾ (V
× V))𝑥 ∧ 𝑝 ∈ 𝐴) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
33 | 22, 32 | bitri 275 |
. . . . 5
⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
34 | 33 | exbii 1851 |
. . . 4
⊢
(∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ ∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑧, 𝑦⟩ ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
35 | 1, 21, 34 | 3bitr4i 303 |
. . 3
⊢
(∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥)) |
36 | 16 | eldm2 5862 |
. . 3
⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴) |
37 | 16 | elima2 6024 |
. . 3
⊢ (𝑥 ∈ ((1st ↾
(V × V)) “ 𝐴)
↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥)) |
38 | 35, 36, 37 | 3bitr4i 303 |
. 2
⊢ (𝑥 ∈ dom 𝐴 ↔ 𝑥 ∈ ((1st ↾ (V ×
V)) “ 𝐴)) |
39 | 38 | eqriv 2734 |
1
⊢ dom 𝐴 = ((1st ↾ (V
× V)) “ 𝐴) |