Step |
Hyp |
Ref |
Expression |
1 |
|
omex |
⊢ ω ∈ V |
2 |
|
limom |
⊢ Lim ω |
3 |
|
r1lim |
⊢ ( ( ω ∈ V ∧ Lim ω ) → ( 𝑅1 ‘ ω ) = ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) ) |
4 |
1 2 3
|
mp2an |
⊢ ( 𝑅1 ‘ ω ) = ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) |
5 |
|
r1fnon |
⊢ 𝑅1 Fn On |
6 |
|
fnfun |
⊢ ( 𝑅1 Fn On → Fun 𝑅1 ) |
7 |
|
funiunfv |
⊢ ( Fun 𝑅1 → ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) ) |
8 |
5 6 7
|
mp2b |
⊢ ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) |
9 |
4 8
|
eqtri |
⊢ ( 𝑅1 ‘ ω ) = ∪ ( 𝑅1 “ ω ) |
10 |
|
iuneq1 |
⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) ) |
11 |
|
sneq |
⊢ ( 𝑓 = 𝑏 → { 𝑓 } = { 𝑏 } ) |
12 |
|
pweq |
⊢ ( 𝑓 = 𝑏 → 𝒫 𝑓 = 𝒫 𝑏 ) |
13 |
11 12
|
xpeq12d |
⊢ ( 𝑓 = 𝑏 → ( { 𝑓 } × 𝒫 𝑓 ) = ( { 𝑏 } × 𝒫 𝑏 ) ) |
14 |
13
|
cbviunv |
⊢ ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) |
15 |
10 14
|
eqtrdi |
⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) |
16 |
15
|
fveq2d |
⊢ ( 𝑒 = 𝑎 → ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) = ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) ) |
17 |
16
|
cbvmptv |
⊢ ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) = ( 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) ) |
18 |
|
dmeq |
⊢ ( 𝑐 = 𝑎 → dom 𝑐 = dom 𝑎 ) |
19 |
18
|
pweqd |
⊢ ( 𝑐 = 𝑎 → 𝒫 dom 𝑐 = 𝒫 dom 𝑎 ) |
20 |
|
imaeq1 |
⊢ ( 𝑐 = 𝑎 → ( 𝑐 “ 𝑑 ) = ( 𝑎 “ 𝑑 ) ) |
21 |
20
|
fveq2d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) |
22 |
19 21
|
mpteq12dv |
⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) ) |
23 |
|
imaeq2 |
⊢ ( 𝑑 = 𝑏 → ( 𝑎 “ 𝑑 ) = ( 𝑎 “ 𝑏 ) ) |
24 |
23
|
fveq2d |
⊢ ( 𝑑 = 𝑏 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) |
25 |
24
|
cbvmptv |
⊢ ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) |
26 |
22 25
|
eqtrdi |
⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) ) |
27 |
26
|
cbvmptv |
⊢ ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) ) |
28 |
|
eqid |
⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) = ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) |
29 |
17 27 28
|
ackbij2 |
⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω |
30 |
|
fvex |
⊢ ( 𝑅1 ‘ ω ) ∈ V |
31 |
9 30
|
eqeltrri |
⊢ ∪ ( 𝑅1 “ ω ) ∈ V |
32 |
31
|
f1oen |
⊢ ( ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω → ∪ ( 𝑅1 “ ω ) ≈ ω ) |
33 |
29 32
|
ax-mp |
⊢ ∪ ( 𝑅1 “ ω ) ≈ ω |
34 |
9 33
|
eqbrtri |
⊢ ( 𝑅1 ‘ ω ) ≈ ω |