Metamath Proof Explorer

Theorem r1om

Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also r1omALT . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion r1om 
|- ( R1 ` _om ) ~~ _om

Proof

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