Metamath Proof Explorer

Theorem hfom

Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also hfomALT . (Contributed by Stefan O'Rear, 18-Nov-2014) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

Ref Expression
Assertion hfom 
|- HF ~~ _om

Proof

Step Hyp Ref Expression
1 iuneq1 
 |-  ( e = a -> U_ f e. e ( { f } X. ~P f ) = U_ f e. a ( { f } X. ~P f ) )
2 sneq 
 |-  ( f = b -> { f } = { b } )
3 pweq 
 |-  ( f = b -> ~P f = ~P b )
4 2 3 xpeq12d 
 |-  ( f = b -> ( { f } X. ~P f ) = ( { b } X. ~P b ) )
5 4 cbviunv 
 |-  U_ f e. a ( { f } X. ~P f ) = U_ b e. a ( { b } X. ~P b )
6 1 5 eqtrdi 
 |-  ( e = a -> U_ f e. e ( { f } X. ~P f ) = U_ b e. a ( { b } X. ~P b ) )
7 6 fveq2d 
 |-  ( e = a -> ( card ` U_ f e. e ( { f } X. ~P f ) ) = ( card ` U_ b e. a ( { b } X. ~P b ) ) )
8 7 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 ) ) )
9 dmeq 
 |-  ( c = a -> dom c = dom a )
10 9 pweqd 
 |-  ( c = a -> ~P dom c = ~P dom a )
11 imaeq1 
 |-  ( c = a -> ( c " d ) = ( a " d ) )
12 11 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 ) ) )
13 10 12 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 ) ) ) )
14 imaeq2 
 |-  ( d = b -> ( a " d ) = ( a " b ) )
15 14 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 ) ) )
16 15 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 ) ) )
17 13 16 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 ) ) ) )
18 17 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 ) ) ) )
19 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 )
20 8 18 19 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 ) : HF -1-1-onto-> _om
21 dfhf2 
 |-  HF = ( R1 ` _om )
22 21 fvexi 
 |-  HF e. _V
23 22 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 ) : HF -1-1-onto-> _om -> HF ~~ _om )
24 20 23 ax-mp 
 |-  HF ~~ _om