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)

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 : U. ( R1 " _om ) -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 ) : U. ( R1 " _om ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U. ( R1 " _om ) -1-1-> _om ) )
36 32 34 35 mp2b 
 |-  ( U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U. ( R1 " _om ) -1-1-> _om )
37 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
38 37 simpli 
 |-  Fun R1
39 funiunfv 
 |-  ( Fun R1 -> U_ a e. _om ( R1 ` a ) = U. ( R1 " _om ) )
40 f1eq2 
 |-  ( U_ a e. _om ( R1 ` a ) = U. ( R1 " _om ) -> ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U. ( R1 " _om ) -1-1-> _om ) )
41 38 39 40 mp2b 
 |-  ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U. ( R1 " _om ) -1-1-> _om )
42 36 41 bitr4i 
 |-  ( U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om )
43 31 42 mpbir 
 |-  U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-> _om
44 rnuni 
 |-  ran U. ( rec ( G , (/) ) " _om ) = U_ a e. ( rec ( G , (/) ) " _om ) ran a
45 eliun 
 |-  ( b e. U_ a e. ( rec ( G , (/) ) " _om ) ran a <-> E. a e. ( rec ( G , (/) ) " _om ) b e. ran a )
46 df-rex 
 |-  ( E. a e. ( rec ( G , (/) ) " _om ) b e. ran a <-> E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) )
47 funfn 
 |-  ( Fun rec ( G , (/) ) <-> rec ( G , (/) ) Fn dom rec ( G , (/) ) )
48 32 47 mpbi 
 |-  rec ( G , (/) ) Fn dom rec ( G , (/) )
49 rdgdmlim 
 |-  Lim dom rec ( G , (/) )
50 limomss 
 |-  ( Lim dom rec ( G , (/) ) -> _om C_ dom rec ( G , (/) ) )
51 49 50 ax-mp 
 |-  _om C_ dom rec ( G , (/) )
52 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 ) )
53 48 51 52 mp2an 
 |-  ( a e. ( rec ( G , (/) ) " _om ) <-> E. c e. _om ( rec ( G , (/) ) ` c ) = a )
54 1 2 ackbij2lem2 
 |-  ( c e. _om -> ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -1-1-onto-> ( card ` ( R1 ` c ) ) )
55 f1ofo 
 |-  ( ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -1-1-onto-> ( card ` ( R1 ` c ) ) -> ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -onto-> ( card ` ( R1 ` c ) ) )
56 forn 
 |-  ( ( rec ( G , (/) ) ` c ) : ( R1 ` c ) -onto-> ( card ` ( R1 ` c ) ) -> ran ( rec ( G , (/) ) ` c ) = ( card ` ( R1 ` c ) ) )
57 54 55 56 3syl 
 |-  ( c e. _om -> ran ( rec ( G , (/) ) ` c ) = ( card ` ( R1 ` c ) ) )
58 r1fin 
 |-  ( c e. _om -> ( R1 ` c ) e. Fin )
59 ficardom 
 |-  ( ( R1 ` c ) e. Fin -> ( card ` ( R1 ` c ) ) e. _om )
60 58 59 syl 
 |-  ( c e. _om -> ( card ` ( R1 ` c ) ) e. _om )
61 ordelss 
 |-  ( ( Ord _om /\ ( card ` ( R1 ` c ) ) e. _om ) -> ( card ` ( R1 ` c ) ) C_ _om )
62 10 60 61 sylancr 
 |-  ( c e. _om -> ( card ` ( R1 ` c ) ) C_ _om )
63 57 62 eqsstrd 
 |-  ( c e. _om -> ran ( rec ( G , (/) ) ` c ) C_ _om )
64 rneq 
 |-  ( ( rec ( G , (/) ) ` c ) = a -> ran ( rec ( G , (/) ) ` c ) = ran a )
65 64 sseq1d 
 |-  ( ( rec ( G , (/) ) ` c ) = a -> ( ran ( rec ( G , (/) ) ` c ) C_ _om <-> ran a C_ _om ) )
66 63 65 syl5ibcom 
 |-  ( c e. _om -> ( ( rec ( G , (/) ) ` c ) = a -> ran a C_ _om ) )
67 66 rexlimiv 
 |-  ( E. c e. _om ( rec ( G , (/) ) ` c ) = a -> ran a C_ _om )
68 53 67 sylbi 
 |-  ( a e. ( rec ( G , (/) ) " _om ) -> ran a C_ _om )
69 68 sselda 
 |-  ( ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) -> b e. _om )
70 69 exlimiv 
 |-  ( E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) -> b e. _om )
71 peano2 
 |-  ( b e. _om -> suc b e. _om )
72 fnfvima 
 |-  ( ( rec ( G , (/) ) Fn dom rec ( G , (/) ) /\ _om C_ dom rec ( G , (/) ) /\ suc b e. _om ) -> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) )
73 48 51 71 72 mp3an12i 
 |-  ( b e. _om -> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) )
74 vex 
 |-  b e. _V
75 cardnn 
 |-  ( suc b e. _om -> ( card ` suc b ) = suc b )
76 fvex 
 |-  ( R1 ` suc b ) e. _V
77 37 simpri 
 |-  Lim dom R1
78 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
79 77 78 ax-mp 
 |-  _om C_ dom R1
80 79 sseli 
 |-  ( suc b e. _om -> suc b e. dom R1 )
81 onssr1 
 |-  ( suc b e. dom R1 -> suc b C_ ( R1 ` suc b ) )
82 80 81 syl 
 |-  ( suc b e. _om -> suc b C_ ( R1 ` suc b ) )
83 ssdomg 
 |-  ( ( R1 ` suc b ) e. _V -> ( suc b C_ ( R1 ` suc b ) -> suc b ~<_ ( R1 ` suc b ) ) )
84 76 82 83 mpsyl 
 |-  ( suc b e. _om -> suc b ~<_ ( R1 ` suc b ) )
85 nnon 
 |-  ( suc b e. _om -> suc b e. On )
86 onenon 
 |-  ( suc b e. On -> suc b e. dom card )
87 85 86 syl 
 |-  ( suc b e. _om -> suc b e. dom card )
88 r1fin 
 |-  ( suc b e. _om -> ( R1 ` suc b ) e. Fin )
89 finnum 
 |-  ( ( R1 ` suc b ) e. Fin -> ( R1 ` suc b ) e. dom card )
90 88 89 syl 
 |-  ( suc b e. _om -> ( R1 ` suc b ) e. dom card )
91 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 ) ) )
92 87 90 91 syl2anc 
 |-  ( suc b e. _om -> ( ( card ` suc b ) C_ ( card ` ( R1 ` suc b ) ) <-> suc b ~<_ ( R1 ` suc b ) ) )
93 84 92 mpbird 
 |-  ( suc b e. _om -> ( card ` suc b ) C_ ( card ` ( R1 ` suc b ) ) )
94 75 93 eqsstrrd 
 |-  ( suc b e. _om -> suc b C_ ( card ` ( R1 ` suc b ) ) )
95 71 94 syl 
 |-  ( b e. _om -> suc b C_ ( card ` ( R1 ` suc b ) ) )
96 sucssel 
 |-  ( b e. _V -> ( suc b C_ ( card ` ( R1 ` suc b ) ) -> b e. ( card ` ( R1 ` suc b ) ) ) )
97 74 95 96 mpsyl 
 |-  ( b e. _om -> b e. ( card ` ( R1 ` suc b ) ) )
98 1 2 ackbij2lem2 
 |-  ( suc b e. _om -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) )
99 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 ) ) )
100 forn 
 |-  ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -onto-> ( card ` ( R1 ` suc b ) ) -> ran ( rec ( G , (/) ) ` suc b ) = ( card ` ( R1 ` suc b ) ) )
101 71 98 99 100 4syl 
 |-  ( b e. _om -> ran ( rec ( G , (/) ) ` suc b ) = ( card ` ( R1 ` suc b ) ) )
102 97 101 eleqtrrd 
 |-  ( b e. _om -> b e. ran ( rec ( G , (/) ) ` suc b ) )
103 fvex 
 |-  ( rec ( G , (/) ) ` suc b ) e. _V
104 eleq1 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ( a e. ( rec ( G , (/) ) " _om ) <-> ( rec ( G , (/) ) ` suc b ) e. ( rec ( G , (/) ) " _om ) ) )
105 rneq 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ran a = ran ( rec ( G , (/) ) ` suc b ) )
106 105 eleq2d 
 |-  ( a = ( rec ( G , (/) ) ` suc b ) -> ( b e. ran a <-> b e. ran ( rec ( G , (/) ) ` suc b ) ) )
107 104 106 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 ) ) ) )
108 103 107 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 ) )
109 73 102 108 syl2anc 
 |-  ( b e. _om -> E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) )
110 70 109 impbii 
 |-  ( E. a ( a e. ( rec ( G , (/) ) " _om ) /\ b e. ran a ) <-> b e. _om )
111 45 46 110 3bitri 
 |-  ( b e. U_ a e. ( rec ( G , (/) ) " _om ) ran a <-> b e. _om )
112 111 eqriv 
 |-  U_ a e. ( rec ( G , (/) ) " _om ) ran a = _om
113 44 112 eqtri 
 |-  ran U. ( rec ( G , (/) ) " _om ) = _om
114 dff1o5 
 |-  ( U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om <-> ( U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-> _om /\ ran U. ( rec ( G , (/) ) " _om ) = _om ) )
115 43 113 114 mpbir2an 
 |-  U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om
116 f1oeq1 
 |-  ( H = U. ( rec ( G , (/) ) " _om ) -> ( H : U. ( R1 " _om ) -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om ) )
117 3 116 ax-mp 
 |-  ( H : U. ( R1 " _om ) -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : U. ( R1 " _om ) -1-1-onto-> _om )
118 115 117 mpbir 
 |-  H : U. ( R1 " _om ) -1-1-onto-> _om