Step |
Hyp |
Ref |
Expression |
1 |
|
omex |
|- _om e. _V |
2 |
|
limom |
|- Lim _om |
3 |
|
r1lim |
|- ( ( _om e. _V /\ Lim _om ) -> ( R1 ` _om ) = U_ a e. _om ( R1 ` a ) ) |
4 |
1 2 3
|
mp2an |
|- ( R1 ` _om ) = U_ a e. _om ( R1 ` a ) |
5 |
|
r1fnon |
|- R1 Fn On |
6 |
|
fnfun |
|- ( R1 Fn On -> Fun R1 ) |
7 |
|
funiunfv |
|- ( Fun R1 -> U_ a e. _om ( R1 ` a ) = U. ( R1 " _om ) ) |
8 |
5 6 7
|
mp2b |
|- U_ a e. _om ( R1 ` a ) = U. ( R1 " _om ) |
9 |
4 8
|
eqtri |
|- ( R1 ` _om ) = U. ( R1 " _om ) |
10 |
|
iuneq1 |
|- ( e = a -> U_ f e. e ( { f } X. ~P f ) = U_ f e. a ( { f } X. ~P f ) ) |
11 |
|
sneq |
|- ( f = b -> { f } = { b } ) |
12 |
|
pweq |
|- ( f = b -> ~P f = ~P b ) |
13 |
11 12
|
xpeq12d |
|- ( f = b -> ( { f } X. ~P f ) = ( { b } X. ~P b ) ) |
14 |
13
|
cbviunv |
|- U_ f e. a ( { f } X. ~P f ) = U_ b e. a ( { b } X. ~P b ) |
15 |
10 14
|
eqtrdi |
|- ( e = a -> U_ f e. e ( { f } X. ~P f ) = U_ b e. a ( { b } X. ~P b ) ) |
16 |
15
|
fveq2d |
|- ( e = a -> ( card ` U_ f e. e ( { f } X. ~P f ) ) = ( card ` U_ b e. a ( { b } X. ~P b ) ) ) |
17 |
16
|
cbvmptv |
|- ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) = ( a e. ( ~P _om i^i Fin ) |-> ( card ` U_ b e. a ( { b } X. ~P b ) ) ) |
18 |
|
dmeq |
|- ( c = a -> dom c = dom a ) |
19 |
18
|
pweqd |
|- ( c = a -> ~P dom c = ~P dom a ) |
20 |
|
imaeq1 |
|- ( c = a -> ( c " d ) = ( a " d ) ) |
21 |
20
|
fveq2d |
|- ( c = a -> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) = ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " d ) ) ) |
22 |
19 21
|
mpteq12dv |
|- ( c = a -> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) = ( d e. ~P dom a |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " d ) ) ) ) |
23 |
|
imaeq2 |
|- ( d = b -> ( a " d ) = ( a " b ) ) |
24 |
23
|
fveq2d |
|- ( d = b -> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " d ) ) = ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " b ) ) ) |
25 |
24
|
cbvmptv |
|- ( d e. ~P dom a |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " d ) ) ) = ( b e. ~P dom a |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " b ) ) ) |
26 |
22 25
|
eqtrdi |
|- ( c = a -> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) = ( b e. ~P dom a |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " b ) ) ) ) |
27 |
26
|
cbvmptv |
|- ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) = ( a e. _V |-> ( b e. ~P dom a |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( a " b ) ) ) ) |
28 |
|
eqid |
|- U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) = U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) |
29 |
17 27 28
|
ackbij2 |
|- U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om |
30 |
|
fvex |
|- ( R1 ` _om ) e. _V |
31 |
9 30
|
eqeltrri |
|- U. ( R1 " _om ) e. _V |
32 |
31
|
f1oen |
|- ( U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om -> U. ( R1 " _om ) ~~ _om ) |
33 |
29 32
|
ax-mp |
|- U. ( R1 " _om ) ~~ _om |
34 |
9 33
|
eqbrtri |
|- ( R1 ` _om ) ~~ _om |