| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | omex 9683 | . . . 4
⊢ ω
∈ V | 
| 2 |  | limom 7903 | . . . 4
⊢ Lim
ω | 
| 3 |  | r1lim 9812 | . . . 4
⊢ ((ω
∈ V ∧ Lim ω) → (𝑅1‘ω) =
∪ 𝑎 ∈ ω
(𝑅1‘𝑎)) | 
| 4 | 1, 2, 3 | mp2an 692 | . . 3
⊢
(𝑅1‘ω) = ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) | 
| 5 |  | r1fnon 9807 | . . . 4
⊢
𝑅1 Fn On | 
| 6 |  | fnfun 6668 | . . . 4
⊢
(𝑅1 Fn On → Fun
𝑅1) | 
| 7 |  | funiunfv 7268 | . . . 4
⊢ (Fun
𝑅1 → ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω)) | 
| 8 | 5, 6, 7 | mp2b 10 | . . 3
⊢ ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω) | 
| 9 | 4, 8 | eqtri 2765 | . 2
⊢
(𝑅1‘ω) = ∪
(𝑅1 “ ω) | 
| 10 |  | iuneq1 5008 | . . . . . . 7
⊢ (𝑒 = 𝑎 → ∪
𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓) = ∪ 𝑓 ∈ 𝑎 ({𝑓} × 𝒫 𝑓)) | 
| 11 |  | sneq 4636 | . . . . . . . . 9
⊢ (𝑓 = 𝑏 → {𝑓} = {𝑏}) | 
| 12 |  | pweq 4614 | . . . . . . . . 9
⊢ (𝑓 = 𝑏 → 𝒫 𝑓 = 𝒫 𝑏) | 
| 13 | 11, 12 | xpeq12d 5716 | . . . . . . . 8
⊢ (𝑓 = 𝑏 → ({𝑓} × 𝒫 𝑓) = ({𝑏} × 𝒫 𝑏)) | 
| 14 | 13 | cbviunv 5040 | . . . . . . 7
⊢ ∪ 𝑓 ∈ 𝑎 ({𝑓} × 𝒫 𝑓) = ∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏) | 
| 15 | 10, 14 | eqtrdi 2793 | . . . . . 6
⊢ (𝑒 = 𝑎 → ∪
𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓) = ∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏)) | 
| 16 | 15 | fveq2d 6910 | . . . . 5
⊢ (𝑒 = 𝑎 → (card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)) = (card‘∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏))) | 
| 17 | 16 | cbvmptv 5255 | . . . 4
⊢ (𝑒 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓))) = (𝑎 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏))) | 
| 18 |  | dmeq 5914 | . . . . . . . 8
⊢ (𝑐 = 𝑎 → dom 𝑐 = dom 𝑎) | 
| 19 | 18 | pweqd 4617 | . . . . . . 7
⊢ (𝑐 = 𝑎 → 𝒫 dom 𝑐 = 𝒫 dom 𝑎) | 
| 20 |  | imaeq1 6073 | . . . . . . . 8
⊢ (𝑐 = 𝑎 → (𝑐 “ 𝑑) = (𝑎 “ 𝑑)) | 
| 21 | 20 | fveq2d 6910 | . . . . . . 7
⊢ (𝑐 = 𝑎 → ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)) = ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑))) | 
| 22 | 19, 21 | mpteq12dv 5233 | . . . . . 6
⊢ (𝑐 = 𝑎 → (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑))) = (𝑑 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑)))) | 
| 23 |  | imaeq2 6074 | . . . . . . . 8
⊢ (𝑑 = 𝑏 → (𝑎 “ 𝑑) = (𝑎 “ 𝑏)) | 
| 24 | 23 | fveq2d 6910 | . . . . . . 7
⊢ (𝑑 = 𝑏 → ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑)) = ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏))) | 
| 25 | 24 | cbvmptv 5255 | . . . . . 6
⊢ (𝑑 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑))) = (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏))) | 
| 26 | 22, 25 | eqtrdi 2793 | . . . . 5
⊢ (𝑐 = 𝑎 → (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑))) = (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏)))) | 
| 27 | 26 | cbvmptv 5255 | . . . 4
⊢ (𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))) = (𝑎 ∈ V ↦ (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏)))) | 
| 28 |  | eqid 2737 | . . . 4
⊢ ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω) = ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “
ω) | 
| 29 | 17, 27, 28 | ackbij2 10282 | . . 3
⊢ ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω | 
| 30 |  | fvex 6919 | . . . . 5
⊢
(𝑅1‘ω) ∈ V | 
| 31 | 9, 30 | eqeltrri 2838 | . . . 4
⊢ ∪ (𝑅1 “ ω) ∈
V | 
| 32 | 31 | f1oen 9013 | . . 3
⊢ (∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω → ∪
(𝑅1 “ ω) ≈ ω) | 
| 33 | 29, 32 | ax-mp 5 | . 2
⊢ ∪ (𝑅1 “ ω) ≈
ω | 
| 34 | 9, 33 | eqbrtri 5164 | 1
⊢
(𝑅1‘ω) ≈ ω |