Step | Hyp | Ref
| Expression |
1 | | excom 2029 |
. . . 4
⊢
(∃𝑦∃𝑝∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑝∃𝑦∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
2 | | opex 4859 |
. . . . . . . 8
⊢
〈𝑧, 𝑦〉 ∈ V |
3 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑧, 𝑦〉 → (𝑝1st 𝑥 ↔ 〈𝑧, 𝑦〉1st 𝑥)) |
4 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑧, 𝑦〉 → (𝑝 ∈ 𝐴 ↔ 〈𝑧, 𝑦〉 ∈ 𝐴)) |
5 | 3, 4 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑧, 𝑦〉 → ((𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴) ↔ (〈𝑧, 𝑦〉1st 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴))) |
6 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
7 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
8 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
9 | 6, 7, 8 | br1steq 30917 |
. . . . . . . . . . 11
⊢
(〈𝑧, 𝑦〉1st 𝑥 ↔ 𝑥 = 𝑧) |
10 | | equcom 1932 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
11 | 9, 10 | bitri 263 |
. . . . . . . . . 10
⊢
(〈𝑧, 𝑦〉1st 𝑥 ↔ 𝑧 = 𝑥) |
12 | 11 | anbi1i 727 |
. . . . . . . . 9
⊢
((〈𝑧, 𝑦〉1st 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴) ↔ (𝑧 = 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴)) |
13 | 5, 12 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑝 = 〈𝑧, 𝑦〉 → ((𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴) ↔ (𝑧 = 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴))) |
14 | 2, 13 | ceqsexv 3215 |
. . . . . . 7
⊢
(∃𝑝(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ (𝑧 = 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴)) |
15 | 14 | exbii 1764 |
. . . . . 6
⊢
(∃𝑧∃𝑝(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴)) |
16 | | excom 2029 |
. . . . . 6
⊢
(∃𝑧∃𝑝(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ ∃𝑝∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
17 | | opeq1 4340 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → 〈𝑧, 𝑦〉 = 〈𝑥, 𝑦〉) |
18 | 17 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (〈𝑧, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
19 | 8, 18 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑧(𝑧 = 𝑥 ∧ 〈𝑧, 𝑦〉 ∈ 𝐴) ↔ 〈𝑥, 𝑦〉 ∈ 𝐴) |
20 | 15, 16, 19 | 3bitr3ri 290 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ∃𝑝∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
21 | 20 | exbii 1764 |
. . . 4
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ∃𝑦∃𝑝∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
22 | | ancom 465 |
. . . . . 6
⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ (𝑝(1st ↾ (V × V))𝑥 ∧ 𝑝 ∈ 𝐴)) |
23 | | anass 679 |
. . . . . . 7
⊢
(((∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝1st 𝑥) ∧ 𝑝 ∈ 𝐴) ↔ (∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
24 | 8 | brres 5323 |
. . . . . . . . 9
⊢ (𝑝(1st ↾ (V
× V))𝑥 ↔ (𝑝1st 𝑥 ∧ 𝑝 ∈ (V × V))) |
25 | | ancom 465 |
. . . . . . . . . 10
⊢ ((𝑝1st 𝑥 ∧ 𝑝 ∈ (V × V)) ↔ (𝑝 ∈ (V × V) ∧
𝑝1st 𝑥)) |
26 | | elvv 5100 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (V × V) ↔
∃𝑧∃𝑦 𝑝 = 〈𝑧, 𝑦〉) |
27 | | excom 2029 |
. . . . . . . . . . . 12
⊢
(∃𝑧∃𝑦 𝑝 = 〈𝑧, 𝑦〉 ↔ ∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉) |
28 | 26, 27 | bitri 263 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (V × V) ↔
∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉) |
29 | 28 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (V × V) ∧
𝑝1st 𝑥) ↔ (∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝1st 𝑥)) |
30 | 25, 29 | bitri 263 |
. . . . . . . . 9
⊢ ((𝑝1st 𝑥 ∧ 𝑝 ∈ (V × V)) ↔ (∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝1st 𝑥)) |
31 | 24, 30 | bitri 263 |
. . . . . . . 8
⊢ (𝑝(1st ↾ (V
× V))𝑥 ↔
(∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝1st 𝑥)) |
32 | 31 | anbi1i 727 |
. . . . . . 7
⊢ ((𝑝(1st ↾ (V
× V))𝑥 ∧ 𝑝 ∈ 𝐴) ↔ ((∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ 𝑝1st 𝑥) ∧ 𝑝 ∈ 𝐴)) |
33 | | 19.41vv 1902 |
. . . . . . 7
⊢
(∃𝑦∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴)) ↔ (∃𝑦∃𝑧 𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
34 | 23, 32, 33 | 3bitr4i 291 |
. . . . . 6
⊢ ((𝑝(1st ↾ (V
× V))𝑥 ∧ 𝑝 ∈ 𝐴) ↔ ∃𝑦∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
35 | 22, 34 | bitri 263 |
. . . . 5
⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ ∃𝑦∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
36 | 35 | exbii 1764 |
. . . 4
⊢
(∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥) ↔ ∃𝑝∃𝑦∃𝑧(𝑝 = 〈𝑧, 𝑦〉 ∧ (𝑝1st 𝑥 ∧ 𝑝 ∈ 𝐴))) |
37 | 1, 21, 36 | 3bitr4i 291 |
. . 3
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥)) |
38 | 8 | eldm2 5244 |
. . 3
⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
39 | 8 | elima2 5391 |
. . 3
⊢ (𝑥 ∈ ((1st ↾
(V × V)) “ 𝐴)
↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ 𝑝(1st ↾ (V × V))𝑥)) |
40 | 37, 38, 39 | 3bitr4i 291 |
. 2
⊢ (𝑥 ∈ dom 𝐴 ↔ 𝑥 ∈ ((1st ↾ (V ×
V)) “ 𝐴)) |
41 | 40 | eqriv 2607 |
1
⊢ dom 𝐴 = ((1st ↾ (V
× V)) “ 𝐴) |