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