Step | Hyp | Ref
| Expression |
1 | | omex 8837 |
. . . 4
⊢ ω
∈ V |
2 | | limom 7358 |
. . . 4
⊢ Lim
ω |
3 | | r1lim 8932 |
. . . 4
⊢ ((ω
∈ V ∧ Lim ω) → (𝑅1‘ω) =
∪ 𝑎 ∈ ω
(𝑅1‘𝑎)) |
4 | 1, 2, 3 | mp2an 682 |
. . 3
⊢
(𝑅1‘ω) = ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) |
5 | | r1fnon 8927 |
. . . 4
⊢
𝑅1 Fn On |
6 | | fnfun 6233 |
. . . 4
⊢
(𝑅1 Fn On → Fun
𝑅1) |
7 | | funiunfv 6778 |
. . . 4
⊢ (Fun
𝑅1 → ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω)) |
8 | 5, 6, 7 | mp2b 10 |
. . 3
⊢ ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω) |
9 | 4, 8 | eqtri 2801 |
. 2
⊢
(𝑅1‘ω) = ∪
(𝑅1 “ ω) |
10 | | iuneq1 4767 |
. . . . . . 7
⊢ (𝑒 = 𝑎 → ∪
𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓) = ∪ 𝑓 ∈ 𝑎 ({𝑓} × 𝒫 𝑓)) |
11 | | sneq 4407 |
. . . . . . . . 9
⊢ (𝑓 = 𝑏 → {𝑓} = {𝑏}) |
12 | | pweq 4381 |
. . . . . . . . 9
⊢ (𝑓 = 𝑏 → 𝒫 𝑓 = 𝒫 𝑏) |
13 | 11, 12 | xpeq12d 5386 |
. . . . . . . 8
⊢ (𝑓 = 𝑏 → ({𝑓} × 𝒫 𝑓) = ({𝑏} × 𝒫 𝑏)) |
14 | 13 | cbviunv 4792 |
. . . . . . 7
⊢ ∪ 𝑓 ∈ 𝑎 ({𝑓} × 𝒫 𝑓) = ∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏) |
15 | 10, 14 | syl6eq 2829 |
. . . . . 6
⊢ (𝑒 = 𝑎 → ∪
𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓) = ∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏)) |
16 | 15 | fveq2d 6450 |
. . . . 5
⊢ (𝑒 = 𝑎 → (card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)) = (card‘∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏))) |
17 | 16 | cbvmptv 4985 |
. . . 4
⊢ (𝑒 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓))) = (𝑎 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑏 ∈ 𝑎 ({𝑏} × 𝒫 𝑏))) |
18 | | dmeq 5569 |
. . . . . . . 8
⊢ (𝑐 = 𝑎 → dom 𝑐 = dom 𝑎) |
19 | 18 | pweqd 4383 |
. . . . . . 7
⊢ (𝑐 = 𝑎 → 𝒫 dom 𝑐 = 𝒫 dom 𝑎) |
20 | | imaeq1 5715 |
. . . . . . . 8
⊢ (𝑐 = 𝑎 → (𝑐 “ 𝑑) = (𝑎 “ 𝑑)) |
21 | 20 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑐 = 𝑎 → ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)) = ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑))) |
22 | 19, 21 | mpteq12dv 4969 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑))) = (𝑑 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑)))) |
23 | | imaeq2 5716 |
. . . . . . . 8
⊢ (𝑑 = 𝑏 → (𝑎 “ 𝑑) = (𝑎 “ 𝑏)) |
24 | 23 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑑 = 𝑏 → ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑)) = ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏))) |
25 | 24 | cbvmptv 4985 |
. . . . . 6
⊢ (𝑑 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑑))) = (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏))) |
26 | 22, 25 | syl6eq 2829 |
. . . . 5
⊢ (𝑐 = 𝑎 → (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑))) = (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏)))) |
27 | 26 | cbvmptv 4985 |
. . . 4
⊢ (𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))) = (𝑎 ∈ V ↦ (𝑏 ∈ 𝒫 dom 𝑎 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑎 “ 𝑏)))) |
28 | | eqid 2777 |
. . . 4
⊢ ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω) = ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “
ω) |
29 | 17, 27, 28 | ackbij2 9400 |
. . 3
⊢ ∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω |
30 | | fvex 6459 |
. . . . 5
⊢
(𝑅1‘ω) ∈ V |
31 | 9, 30 | eqeltrri 2855 |
. . . 4
⊢ ∪ (𝑅1 “ ω) ∈
V |
32 | 31 | f1oen 8262 |
. . 3
⊢ (∪ (rec((𝑐 ∈ V ↦ (𝑑 ∈ 𝒫 dom 𝑐 ↦ ((𝑒 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑒 ({𝑓} × 𝒫 𝑓)))‘(𝑐 “ 𝑑)))), ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω → ∪
(𝑅1 “ ω) ≈ ω) |
33 | 29, 32 | ax-mp 5 |
. 2
⊢ ∪ (𝑅1 “ ω) ≈
ω |
34 | 9, 33 | eqbrtri 4907 |
1
⊢
(𝑅1‘ω) ≈ ω |