Metamath Proof Explorer

Theorem ackbij2

Description: The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

Ref Expression
Hypotheses ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
ackbij.g 
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
ackbij.h 
|- H = U. ( rec ( G , (/) ) " _om )
Assertion ackbij2 
|- H : HF -1-1-onto-> _om

Proof

Step Hyp Ref Expression
1 ackbij.f 
 |-  F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
2 ackbij.g 
 |-  G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
3 ackbij.h 
 |-  H = U. ( rec ( G , (/) ) " _om )
4 fveq2 
 |-  ( a = b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` b ) )
5 fvex 
 |-  ( rec ( G , (/) ) ` a ) e. _V
6 4 5 f1iun 
 |-  ( A. a e. _om ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> _om /\ A. b e. _om ( ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) \/ ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) ) -> U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om )
7 1 2 ackbij2lem2 
 |-  ( a e. _om -> ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) )
8 f1of1 
 |-  ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) -> ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> ( card ` ( R1 ` a ) ) )
9 7 8 syl 
 |-  ( a e. _om -> ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> ( card ` ( R1 ` a ) ) )
10 ordom 
 |-  Ord _om
11 r1fin 
 |-  ( a e. _om -> ( R1 ` a ) e. Fin )
12 ficardom 
 |-  ( ( R1 ` a ) e. Fin -> ( card ` ( R1 ` a ) ) e. _om )
13 11 12 syl 
 |-  ( a e. _om -> ( card ` ( R1 ` a ) ) e. _om )
14 ordelss 
 |-  ( ( Ord _om /\ ( card ` ( R1 ` a ) ) e. _om ) -> ( card ` ( R1 ` a ) ) C_ _om )
15 10 13 14 sylancr 
 |-  ( a e. _om -> ( card ` ( R1 ` a ) ) C_ _om )
16 f1ss 
 |-  ( ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> ( card ` ( R1 ` a ) ) /\ ( card ` ( R1 ` a ) ) C_ _om ) -> ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> _om )
17 9 15 16 syl2anc 
 |-  ( a e. _om -> ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> _om )
18 nnord 
 |-  ( a e. _om -> Ord a )
19 nnord 
 |-  ( b e. _om -> Ord b )
20 ordtri2or2 
 |-  ( ( Ord a /\ Ord b ) -> ( a C_ b \/ b C_ a ) )
21 18 19 20 syl2an 
 |-  ( ( a e. _om /\ b e. _om ) -> ( a C_ b \/ b C_ a ) )
22 1 2 ackbij2lem4 
 |-  ( ( ( b e. _om /\ a e. _om ) /\ a C_ b ) -> ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) )
23 22 ex 
 |-  ( ( b e. _om /\ a e. _om ) -> ( a C_ b -> ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) ) )
24 23 ancoms 
 |-  ( ( a e. _om /\ b e. _om ) -> ( a C_ b -> ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) ) )
25 1 2 ackbij2lem4 
 |-  ( ( ( a e. _om /\ b e. _om ) /\ b C_ a ) -> ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) )
26 25 ex 
 |-  ( ( a e. _om /\ b e. _om ) -> ( b C_ a -> ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) )
27 24 26 orim12d 
 |-  ( ( a e. _om /\ b e. _om ) -> ( ( a C_ b \/ b C_ a ) -> ( ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) \/ ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) ) )
28 21 27 mpd 
 |-  ( ( a e. _om /\ b e. _om ) -> ( ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) \/ ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) )
29 28 ralrimiva 
 |-  ( a e. _om -> A. b e. _om ( ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) \/ ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) )
30 17 29 jca 
 |-  ( a e. _om -> ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-> _om /\ A. b e. _om ( ( rec ( G , (/) ) ` a ) C_ ( rec ( G , (/) ) ` b ) \/ ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` a ) ) ) )
31 6 30 mprg 
 |-  U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om
32 rdgfun 
 |-  Fun rec ( G , (/) )
33 funiunfv 
 |-  ( Fun rec ( G , (/) ) -> U_ a e. _om ( rec ( G , (/) ) ` a ) = U. ( rec ( G , (/) ) " _om ) )
34 33 eqcomd 
 |-  ( Fun rec ( G , (/) ) -> U. ( rec ( G , (/) ) " _om ) = U_ a e. _om ( rec ( G , (/) ) ` a ) )
35 f1eq1 
 |-  ( U. ( rec ( G , (/) ) " _om ) = U_ a e. _om ( rec ( G , (/) ) ` a ) -> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) )
36 32 34 35 mp2b 
 |-  ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om )
37 r1fun 
 |-  Fun R1
38 funiunfv 
 |-  ( Fun R1 -> U_ a e. _om ( R1 ` a ) = U. ( R1 " _om ) )
39 df-hf 
 |-  HF = U. ( R1 " _om )
40 38 39 eqtr4di 
 |-  ( Fun R1 -> U_ a e. _om ( R1 ` a ) = HF )
41 f1eq2 
 |-  ( U_ a e. _om ( R1 ` a ) = HF -> ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) )
42 37 40 41 mp2b 
 |-  ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om )
43 36 42 bitr4i 
 |-  ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om )
44 31 43 mpbir 
 |-  U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om
45 rnuni 
 |-  ran U. ( rec ( G , (/) ) " _om ) = U_ a e. ( rec ( G , (/) ) " _om ) ran a
46 eliun 
 |-  ( b e. U_ a e. ( rec ( G , (/) ) " _om ) ran a <-> E. a e. ( rec ( G , (/) ) " _om ) b e. ran a )
47 df-rex 
 |-  ( E. a e. ( rec ( G , (/) ) " _om ) b e. ran a <-> E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) )
48 funfn 
 |-  ( Fun rec ( G , (/) ) <-> rec ( G , (/) ) Fn dom rec ( G , (/) ) )
49 32 48 mpbi 
 |-  rec ( G , (/) ) Fn dom rec ( G , (/) )
50 rdgdmlim 
 |-  Lim dom rec ( G , (/) )
51 limomss 
 |-  ( Lim dom rec ( G , (/) ) -> _om C_ dom rec ( G , (/) ) )
52 50 51 ax-mp 
 |-  _om C_ dom rec ( G , (/) )
53 fvelimab 
 |-  ( ( rec ( G , (/) ) Fn dom rec ( G , (/) ) /\ _om C_ dom rec ( G , (/) ) ) -> ( a e. ( rec ( G , (/) ) " _om ) <-> E. c e. _om ( rec ( G , (/) ) ` c ) = a ) )
54 49 52 53 mp2an 
 |-  ( a e. ( rec ( G , (/) ) " _om ) <-> E. c e. _om ( rec ( G , (/) ) ` c ) = a )
55 1 2 ackbij2lem2 
 |-  ( c e. _om -> ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -1-1-onto-> ( card ` ( R1 ` c ) ) )
56 f1ofo 
 |-  ( ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -1-1-onto-> ( card ` ( R1 ` c ) ) -> ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -onto-> ( card ` ( R1 ` c ) ) )
57 forn 
 |-  ( ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -onto-> ( card ` ( R1 ` c ) ) -> ran ( rec ( G , (/) ) ` c ) = ( card ` ( R1 ` c ) ) )
58 55 56 57 3syl 
 |-  ( c e. _om -> ran ( rec ( G , (/) ) ` c ) = ( card ` ( R1 ` c ) ) )
59 r1fin 
 |-  ( c e. _om -> ( R1 ` c ) e. Fin )
60 ficardom 
 |-  ( ( R1 ` c ) e. Fin -> ( card ` ( R1 ` c ) ) e. _om )
61 59 60 syl 
 |-  ( c e. _om -> ( card ` ( R1 ` c ) ) e. _om )
62 ordelss 
 |-  ( ( Ord _om /\ ( card ` ( R1 ` c ) ) e. _om ) -> ( card ` ( R1 ` c ) ) C_ _om )
63 10 61 62 sylancr 
 |-  ( c e. _om -> ( card ` ( R1 ` c ) ) C_ _om )
64 58 63 eqsstrd 
 |-  ( c e. _om -> ran ( rec ( G , (/) ) ` c ) C_ _om )
65 rneq 
 |-  ( ( rec ( G , (/) ) ` c ) = a -> ran ( rec ( G , (/) ) ` c ) = ran a )
66 65 sseq1d 
 |-  ( ( rec ( G , (/) ) ` c ) = a -> ( ran ( rec ( G , (/) ) ` c ) C_ _om <-> ran a C_ _om ) )
67 64 66 syl5ibcom 
 |-  ( c e. _om -> ( ( rec ( G , (/) ) ` c ) = a -> ran a C_ _om ) )
68 67 rexlimiv 
 |-  ( E. c e. _om ( rec ( G , (/) ) ` c ) = a -> ran a C_ _om )
69 54 68 sylbi 
 |-  ( a e. ( rec ( G , (/) ) " _om ) -> ran a C_ _om )
70 69 sselda 
 |-  ( ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) -> b e. _om )
71 70 exlimiv 
 |-  ( E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) -> b e. _om )
72 peano2 
 |-  ( b e. _om -> suc b e. _om )
73 fnfvima 
 |-  ( ( rec ( G , (/) ) Fn dom rec ( G , (/) ) /\ _om C_ dom rec ( G , (/) ) /\ suc b e. _om ) -> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) )
74 49 52 72 73 mp3an12i 
 |-  ( b e. _om -> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) )
75 vex 
 |-  b e. _V
76 cardnn 
 |-  ( suc b e. _om -> ( card ` suc b ) = suc b )
77 fvex 
 |-  ( R1 ` suc b ) e. _V
78 r1dmlim 
 |-  Lim dom R1
79 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
80 78 79 ax-mp 
 |-  _om C_ dom R1
81 80 sseli 
 |-  ( suc b e. _om -> suc b e. dom R1 )
82 onssr1 
 |-  ( suc b e. dom R1 -> suc b C_ ( R1 ` suc b ) )
83 81 82 syl 
 |-  ( suc b e. _om -> suc b C_ ( R1 ` suc b ) )
84 ssdomg 
 |-  ( ( R1 ` suc b ) e. _V -> ( suc b C_ ( R1 ` suc b ) -> suc b ~<_ ( R1 ` suc b ) ) )
85 77 83 84 mpsyl 
 |-  ( suc b e. _om -> suc b ~<_ ( R1 ` suc b ) )
86 nnon 
 |-  ( suc b e. _om -> suc b e. On )
87 onenon 
 |-  ( suc b e. On -> suc b e. dom card )
88 86 87 syl 
 |-  ( suc b e. _om -> suc b e. dom card )
89 r1fin 
 |-  ( suc b e. _om -> ( R1 ` suc b ) e. Fin )
90 finnum 
 |-  ( ( R1 ` suc b ) e. Fin -> ( R1 ` suc b ) e. dom card )
91 89 90 syl 
 |-  ( suc b e. _om -> ( R1 ` suc b ) e. dom card )
92 carddom2 
 |-  ( ( suc b e. dom card /\ ( R1 ` suc b ) e. dom card ) -> ( ( card ` suc b ) C_ ( card ` ( R1 ` suc b ) ) <-> suc b ~<_ ( R1 ` suc b ) ) )
93 88 91 92 syl2anc 
 |-  ( suc b e. _om -> ( ( card ` suc b ) C_ ( card ` ( R1 ` suc b ) ) <-> suc b ~<_ ( R1 ` suc b ) ) )
94 85 93 mpbird 
 |-  ( suc b e. _om -> ( card ` suc b ) C_ ( card ` ( R1 ` suc b ) ) )
95 76 94 eqsstrrd 
 |-  ( suc b e. _om -> suc b C_ ( card ` ( R1 ` suc b ) ) )
96 72 95 syl 
 |-  ( b e. _om -> suc b C_ ( card ` ( R1 ` suc b ) ) )
97 sucssel 
 |-  ( b e. _V -> ( suc b C_ ( card ` ( R1 ` suc b ) ) -> b e. ( card ` ( R1 ` suc b ) ) ) )
98 75 96 97 mpsyl 
 |-  ( b e. _om -> b e. ( card ` ( R1 ` suc b ) ) )
99 1 2 ackbij2lem2 
 |-  ( suc b e. _om -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) )
100 f1ofo 
 |-  ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -onto-> ( card ` ( R1 ` suc b ) ) )
101 forn 
 |-  ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -onto-> ( card ` ( R1 ` suc b ) ) -> ran ( rec ( G , (/) ) ` suc b ) = ( card ` ( R1 ` suc b ) ) )
102 72 99 100 101 4syl 
 |-  ( b e. _om -> ran ( rec ( G , (/) ) ` suc b ) = ( card ` ( R1 ` suc b ) ) )
103 98 102 eleqtrrd 
 |-  ( b e. _om -> b e. ran ( rec ( G , (/) ) ` suc b ) )
104 fvex 
 |-  ( rec ( G , (/) ) ` suc b ) e. _V
105 eleq1 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ( a e. ( rec ( G , (/) ) " _om ) <-> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) ) )
106 rneq 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ran a = ran ( rec ( G , (/) ) ` suc b ) )
107 106 eleq2d 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ( b e. ran a <-> b e. ran ( rec ( G , (/) ) ` suc b ) ) )
108 105 107 anbi12d 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ( ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) <-> ( ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) /\ b e. ran ( rec ( G , (/) ) ` suc b ) ) ) )
109 104 108 spcev 
 |-  ( ( ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) /\ b e. ran ( rec ( G , (/) ) ` suc b ) ) -> E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) )
110 74 103 109 syl2anc 
 |-  ( b e. _om -> E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) )
111 71 110 impbii 
 |-  ( E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) <-> b e. _om )
112 46 47 111 3bitri 
 |-  ( b e. U_ a e. ( rec ( G , (/) ) " _om ) ran a <-> b e. _om )
113 112 eqriv 
 |-  U_ a e. ( rec ( G , (/) ) " _om ) ran a = _om
114 45 113 eqtri 
 |-  ran U. ( rec ( G , (/) ) " _om ) = _om
115 dff1o5 
 |-  ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om <-> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om /\ ran U. ( rec ( G , (/) ) " _om ) = _om ) )
116 44 114 115 mpbir2an 
 |-  U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om
117 f1oeq1 
 |-  ( H = U. ( rec ( G , (/) ) " _om ) -> ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om ) )
118 3 117 ax-mp 
 |-  ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om )
119 116 118 mpbir 
 |-  H : HF -1-1-onto-> _om