| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | r111 9816 | . . . 4
⊢
𝑅1:On–1-1→V | 
| 2 |  | omsson 7892 | . . . 4
⊢ ω
⊆ On | 
| 3 |  | f1ores 6861 | . . . 4
⊢
((𝑅1:On–1-1→V ∧ ω ⊆ On) →
(𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “
ω)) | 
| 4 | 1, 2, 3 | mp2an 692 | . . 3
⊢
(𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “
ω) | 
| 5 |  | f1of1 6846 | . . 3
⊢
((𝑅1 ↾ ω):ω–1-1-onto→(𝑅1 “ ω) →
(𝑅1 ↾ ω):ω–1-1→(𝑅1 “
ω)) | 
| 6 | 4, 5 | ax-mp 5 | . 2
⊢
(𝑅1 ↾ ω):ω–1-1→(𝑅1 “
ω) | 
| 7 |  | r1fnon 9808 | . . . . . . . 8
⊢
𝑅1 Fn On | 
| 8 |  | fvelimab 6980 | . . . . . . . 8
⊢
((𝑅1 Fn On ∧ ω ⊆ On) → (𝑤 ∈ (𝑅1
“ ω) ↔ ∃𝑥 ∈ ω
(𝑅1‘𝑥) = 𝑤)) | 
| 9 | 7, 2, 8 | mp2an 692 | . . . . . . 7
⊢ (𝑤 ∈ (𝑅1
“ ω) ↔ ∃𝑥 ∈ ω
(𝑅1‘𝑥) = 𝑤) | 
| 10 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) | 
| 11 | 10 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝑥 = ∅ →
((𝑅1‘𝑥) ∈ 𝑦 ↔ (𝑅1‘∅)
∈ 𝑦)) | 
| 12 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑅1‘𝑥) =
(𝑅1‘𝑤)) | 
| 13 | 12 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → ((𝑅1‘𝑥) ∈ 𝑦 ↔ (𝑅1‘𝑤) ∈ 𝑦)) | 
| 14 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = suc 𝑤 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑤)) | 
| 15 | 14 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝑥 = suc 𝑤 → ((𝑅1‘𝑥) ∈ 𝑦 ↔ (𝑅1‘suc
𝑤) ∈ 𝑦)) | 
| 16 |  | r10 9809 | . . . . . . . . . . . . 13
⊢
(𝑅1‘∅) = ∅ | 
| 17 | 16 | eleq1i 2831 | . . . . . . . . . . . 12
⊢
((𝑅1‘∅) ∈ 𝑦 ↔ ∅ ∈ 𝑦) | 
| 18 | 17 | biimpri 228 | . . . . . . . . . . 11
⊢ (∅
∈ 𝑦 →
(𝑅1‘∅) ∈ 𝑦) | 
| 19 | 18 | adantr 480 | . . . . . . . . . 10
⊢ ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) →
(𝑅1‘∅) ∈ 𝑦) | 
| 20 |  | pweq 4613 | . . . . . . . . . . . . . . 15
⊢ (𝑧 =
(𝑅1‘𝑤) → 𝒫 𝑧 = 𝒫
(𝑅1‘𝑤)) | 
| 21 | 20 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑧 =
(𝑅1‘𝑤) → (𝒫 𝑧 ∈ 𝑦 ↔ 𝒫
(𝑅1‘𝑤) ∈ 𝑦)) | 
| 22 | 21 | rspccv 3618 | . . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝑦 𝒫 𝑧 ∈ 𝑦 → ((𝑅1‘𝑤) ∈ 𝑦 → 𝒫
(𝑅1‘𝑤) ∈ 𝑦)) | 
| 23 |  | nnon 7894 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ω → 𝑤 ∈ On) | 
| 24 |  | r1suc 9811 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ On →
(𝑅1‘suc 𝑤) = 𝒫
(𝑅1‘𝑤)) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ω →
(𝑅1‘suc 𝑤) = 𝒫
(𝑅1‘𝑤)) | 
| 26 | 25 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ω →
((𝑅1‘suc 𝑤) ∈ 𝑦 ↔ 𝒫
(𝑅1‘𝑤) ∈ 𝑦)) | 
| 27 | 26 | biimprcd 250 | . . . . . . . . . . . . 13
⊢
(𝒫 (𝑅1‘𝑤) ∈ 𝑦 → (𝑤 ∈ ω →
(𝑅1‘suc 𝑤) ∈ 𝑦)) | 
| 28 | 22, 27 | syl6 35 | . . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑦 𝒫 𝑧 ∈ 𝑦 → ((𝑅1‘𝑤) ∈ 𝑦 → (𝑤 ∈ ω →
(𝑅1‘suc 𝑤) ∈ 𝑦))) | 
| 29 | 28 | com3r 87 | . . . . . . . . . . 11
⊢ (𝑤 ∈ ω →
(∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ((𝑅1‘𝑤) ∈ 𝑦 → (𝑅1‘suc
𝑤) ∈ 𝑦))) | 
| 30 | 29 | adantld 490 | . . . . . . . . . 10
⊢ (𝑤 ∈ ω → ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → ((𝑅1‘𝑤) ∈ 𝑦 → (𝑅1‘suc
𝑤) ∈ 𝑦))) | 
| 31 | 11, 13, 15, 19, 30 | finds2 7921 | . . . . . . . . 9
⊢ (𝑥 ∈ ω → ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → (𝑅1‘𝑥) ∈ 𝑦)) | 
| 32 |  | eleq1 2828 | . . . . . . . . . 10
⊢
((𝑅1‘𝑥) = 𝑤 → ((𝑅1‘𝑥) ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)) | 
| 33 | 32 | biimpd 229 | . . . . . . . . 9
⊢
((𝑅1‘𝑥) = 𝑤 → ((𝑅1‘𝑥) ∈ 𝑦 → 𝑤 ∈ 𝑦)) | 
| 34 | 31, 33 | syl9 77 | . . . . . . . 8
⊢ (𝑥 ∈ ω →
((𝑅1‘𝑥) = 𝑤 → ((∅ ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → 𝑤 ∈ 𝑦))) | 
| 35 | 34 | rexlimiv 3147 | . . . . . . 7
⊢
(∃𝑥 ∈
ω (𝑅1‘𝑥) = 𝑤 → ((∅ ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → 𝑤 ∈ 𝑦)) | 
| 36 | 9, 35 | sylbi 217 | . . . . . 6
⊢ (𝑤 ∈ (𝑅1
“ ω) → ((∅ ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → 𝑤 ∈ 𝑦)) | 
| 37 | 36 | com12 32 | . . . . 5
⊢ ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → (𝑤 ∈ (𝑅1 “
ω) → 𝑤 ∈
𝑦)) | 
| 38 | 37 | ssrdv 3988 | . . . 4
⊢ ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → (𝑅1 “
ω) ⊆ 𝑦) | 
| 39 |  | vex 3483 | . . . . 5
⊢ 𝑦 ∈ V | 
| 40 | 39 | ssex 5320 | . . . 4
⊢
((𝑅1 “ ω) ⊆ 𝑦 → (𝑅1 “
ω) ∈ V) | 
| 41 | 38, 40 | syl 17 | . . 3
⊢ ((∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) → (𝑅1 “
ω) ∈ V) | 
| 42 |  | 0ex 5306 | . . . 4
⊢ ∅
∈ V | 
| 43 |  | eleq1 2828 | . . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝑦 ↔ ∅ ∈ 𝑦)) | 
| 44 | 43 | anbi1d 631 | . . . . 5
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) ↔ (∅ ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦))) | 
| 45 | 44 | exbidv 1920 | . . . 4
⊢ (𝑥 = ∅ → (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) ↔ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦))) | 
| 46 |  | axgroth6 10869 | . . . . 5
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) | 
| 47 |  | simpr 484 | . . . . . . . 8
⊢
((𝒫 𝑧
⊆ 𝑦 ∧ 𝒫
𝑧 ∈ 𝑦) → 𝒫 𝑧 ∈ 𝑦) | 
| 48 | 47 | ralimi 3082 | . . . . . . 7
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) → ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) | 
| 49 | 48 | anim2i 617 | . . . . . 6
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦)) → (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦)) | 
| 50 | 49 | 3adant3 1132 | . . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) → (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦)) | 
| 51 | 46, 50 | eximii 1836 | . . . 4
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) | 
| 52 | 42, 45, 51 | vtocl 3557 | . . 3
⊢
∃𝑦(∅
∈ 𝑦 ∧
∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) | 
| 53 | 41, 52 | exlimiiv 1930 | . 2
⊢
(𝑅1 “ ω) ∈ V | 
| 54 |  | f1dmex 7982 | . 2
⊢
(((𝑅1 ↾ ω):ω–1-1→(𝑅1 “ ω) ∧
(𝑅1 “ ω) ∈ V) → ω ∈
V) | 
| 55 | 6, 53, 54 | mp2an 692 | 1
⊢ ω
∈ V |