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