Metamath Proof Explorer

Theorem ackbij1

Description: The Ackermann bijection, part 1: each natural number can be uniquely coded in binary as a finite set of natural numbers and conversely. (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion ackbij1 
|- F : ( ~P _om i^i Fin ) -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 1 ackbij1lem17 
 |-  F : ( ~P _om i^i Fin ) -1-1-> _om
3 f1f 
 |-  ( F : ( ~P _om i^i Fin ) -1-1-> _om -> F : ( ~P _om i^i Fin ) --> _om )
4 frn 
 |-  ( F : ( ~P _om i^i Fin ) --> _om -> ran F C_ _om )
5 2 3 4 mp2b 
 |-  ran F C_ _om
6 eleq1 
 |-  ( b = (/) -> ( b e. ran F <-> (/) e. ran F ) )
7 eleq1 
 |-  ( b = a -> ( b e. ran F <-> a e. ran F ) )
8 eleq1 
 |-  ( b = suc a -> ( b e. ran F <-> suc a e. ran F ) )
9 peano1 
 |-  (/) e. _om
10 ackbij1lem3 
 |-  ( (/) e. _om -> (/) e. ( ~P _om i^i Fin ) )
11 9 10 ax-mp 
 |-  (/) e. ( ~P _om i^i Fin )
12 1 ackbij1lem13 
 |-  ( F ` (/) ) = (/)
13 fveqeq2 
 |-  ( a = (/) -> ( ( F ` a ) = (/) <-> ( F ` (/) ) = (/) ) )
14 13 rspcev 
 |-  ( ( (/) e. ( ~P _om i^i Fin ) /\ ( F ` (/) ) = (/) ) -> E. a e. ( ~P _om i^i Fin ) ( F ` a ) = (/) )
15 11 12 14 mp2an 
 |-  E. a e. ( ~P _om i^i Fin ) ( F ` a ) = (/)
16 f1fn 
 |-  ( F : ( ~P _om i^i Fin ) -1-1-> _om -> F Fn ( ~P _om i^i Fin ) )
17 2 16 ax-mp 
 |-  F Fn ( ~P _om i^i Fin )
18 fvelrnb 
 |-  ( F Fn ( ~P _om i^i Fin ) -> ( (/) e. ran F <-> E. a e. ( ~P _om i^i Fin ) ( F ` a ) = (/) ) )
19 17 18 ax-mp 
 |-  ( (/) e. ran F <-> E. a e. ( ~P _om i^i Fin ) ( F ` a ) = (/) )
20 15 19 mpbir 
 |-  (/) e. ran F
21 1 ackbij1lem18 
 |-  ( c e. ( ~P _om i^i Fin ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` c ) )
22 21 adantl 
 |-  ( ( a e. _om /\ c e. ( ~P _om i^i Fin ) ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` c ) )
23 suceq 
 |-  ( ( F ` c ) = a -> suc ( F ` c ) = suc a )
24 23 eqeq2d 
 |-  ( ( F ` c ) = a -> ( ( F ` b ) = suc ( F ` c ) <-> ( F ` b ) = suc a ) )
25 24 rexbidv 
 |-  ( ( F ` c ) = a -> ( E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` c ) <-> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc a ) )
26 22 25 syl5ibcom 
 |-  ( ( a e. _om /\ c e. ( ~P _om i^i Fin ) ) -> ( ( F ` c ) = a -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc a ) )
27 26 rexlimdva 
 |-  ( a e. _om -> ( E. c e. ( ~P _om i^i Fin ) ( F ` c ) = a -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc a ) )
28 fvelrnb 
 |-  ( F Fn ( ~P _om i^i Fin ) -> ( a e. ran F <-> E. c e. ( ~P _om i^i Fin ) ( F ` c ) = a ) )
29 17 28 ax-mp 
 |-  ( a e. ran F <-> E. c e. ( ~P _om i^i Fin ) ( F ` c ) = a )
30 fvelrnb 
 |-  ( F Fn ( ~P _om i^i Fin ) -> ( suc a e. ran F <-> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc a ) )
31 17 30 ax-mp 
 |-  ( suc a e. ran F <-> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc a )
32 27 29 31 3imtr4g 
 |-  ( a e. _om -> ( a e. ran F -> suc a e. ran F ) )
33 6 7 8 7 20 32 finds 
 |-  ( a e. _om -> a e. ran F )
34 33 ssriv 
 |-  _om C_ ran F
35 5 34 eqssi 
 |-  ran F = _om
36 dff1o5 
 |-  ( F : ( ~P _om i^i Fin ) -1-1-onto-> _om <-> ( F : ( ~P _om i^i Fin ) -1-1-> _om /\ ran F = _om ) )
37 2 35 36 mpbir2an 
 |-  F : ( ~P _om i^i Fin ) -1-1-onto-> _om