Metamath Proof Explorer

Theorem ackbij1b

Description: The Ackermann bijection, part 1b: the bijection from ackbij1 restricts naturally to the powers of particular naturals. (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 ackbij1b 
|- ( A e. _om -> ( F " ~P A ) = ( card ` ~P A ) )

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 ackbij2lem1 
 |-  ( A e. _om -> ~P A C_ ( ~P _om i^i Fin ) )
4 pwexg 
 |-  ( A e. _om -> ~P A e. _V )
5 f1imaeng 
 |-  ( ( F : ( ~P _om i^i Fin ) -1-1-> _om /\ ~P A C_ ( ~P _om i^i Fin ) /\ ~P A e. _V ) -> ( F " ~P A ) ~~ ~P A )
6 2 3 4 5 mp3an2i 
 |-  ( A e. _om -> ( F " ~P A ) ~~ ~P A )
7 nnfi 
 |-  ( A e. _om -> A e. Fin )
8 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
9 7 8 sylib 
 |-  ( A e. _om -> ~P A e. Fin )
10 ficardid 
 |-  ( ~P A e. Fin -> ( card ` ~P A ) ~~ ~P A )
11 ensym 
 |-  ( ( card ` ~P A ) ~~ ~P A -> ~P A ~~ ( card ` ~P A ) )
12 9 10 11 3syl 
 |-  ( A e. _om -> ~P A ~~ ( card ` ~P A ) )
13 entr 
 |-  ( ( ( F " ~P A ) ~~ ~P A /\ ~P A ~~ ( card ` ~P A ) ) -> ( F " ~P A ) ~~ ( card ` ~P A ) )
14 6 12 13 syl2anc 
 |-  ( A e. _om -> ( F " ~P A ) ~~ ( card ` ~P A ) )
15 onfin2 
 |-  _om = ( On i^i Fin )
16 inss2 
 |-  ( On i^i Fin ) C_ Fin
17 15 16 eqsstri 
 |-  _om C_ Fin
18 ficardom 
 |-  ( ~P A e. Fin -> ( card ` ~P A ) e. _om )
19 9 18 syl 
 |-  ( A e. _om -> ( card ` ~P A ) e. _om )
20 17 19 sseldi 
 |-  ( A e. _om -> ( card ` ~P A ) e. Fin )
21 php3 
 |-  ( ( ( card ` ~P A ) e. Fin /\ ( F " ~P A ) C. ( card ` ~P A ) ) -> ( F " ~P A ) ~< ( card ` ~P A ) )
22 21 ex 
 |-  ( ( card ` ~P A ) e. Fin -> ( ( F " ~P A ) C. ( card ` ~P A ) -> ( F " ~P A ) ~< ( card ` ~P A ) ) )
23 20 22 syl 
 |-  ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) -> ( F " ~P A ) ~< ( card ` ~P A ) ) )
24 sdomnen 
 |-  ( ( F " ~P A ) ~< ( card ` ~P A ) -> -. ( F " ~P A ) ~~ ( card ` ~P A ) )
25 23 24 syl6 
 |-  ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) -> -. ( F " ~P A ) ~~ ( card ` ~P A ) ) )
26 14 25 mt2d 
 |-  ( A e. _om -> -. ( F " ~P A ) C. ( card ` ~P A ) )
27 fvex 
 |-  ( F ` a ) e. _V
28 ackbij1lem3 
 |-  ( A e. _om -> A e. ( ~P _om i^i Fin ) )
29 elpwi 
 |-  ( a e. ~P A -> a C_ A )
30 1 ackbij1lem12 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a C_ A ) -> ( F ` a ) C_ ( F ` A ) )
31 28 29 30 syl2an 
 |-  ( ( A e. _om /\ a e. ~P A ) -> ( F ` a ) C_ ( F ` A ) )
32 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
33 peano1 
 |-  (/) e. _om
34 32 33 f0cli 
 |-  ( F ` a ) e. _om
35 nnord 
 |-  ( ( F ` a ) e. _om -> Ord ( F ` a ) )
36 34 35 ax-mp 
 |-  Ord ( F ` a )
37 32 33 f0cli 
 |-  ( F ` A ) e. _om
38 nnord 
 |-  ( ( F ` A ) e. _om -> Ord ( F ` A ) )
39 37 38 ax-mp 
 |-  Ord ( F ` A )
40 ordsucsssuc 
 |-  ( ( Ord ( F ` a ) /\ Ord ( F ` A ) ) -> ( ( F ` a ) C_ ( F ` A ) <-> suc ( F ` a ) C_ suc ( F ` A ) ) )
41 36 39 40 mp2an 
 |-  ( ( F ` a ) C_ ( F ` A ) <-> suc ( F ` a ) C_ suc ( F ` A ) )
42 31 41 sylib 
 |-  ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` a ) C_ suc ( F ` A ) )
43 1 ackbij1lem14 
 |-  ( A e. _om -> ( F ` { A } ) = suc ( F ` A ) )
44 1 ackbij1lem8 
 |-  ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) )
45 43 44 eqtr3d 
 |-  ( A e. _om -> suc ( F ` A ) = ( card ` ~P A ) )
46 45 adantr 
 |-  ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` A ) = ( card ` ~P A ) )
47 42 46 sseqtrd 
 |-  ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` a ) C_ ( card ` ~P A ) )
48 sucssel 
 |-  ( ( F ` a ) e. _V -> ( suc ( F ` a ) C_ ( card ` ~P A ) -> ( F ` a ) e. ( card ` ~P A ) ) )
49 27 47 48 mpsyl 
 |-  ( ( A e. _om /\ a e. ~P A ) -> ( F ` a ) e. ( card ` ~P A ) )
50 49 ralrimiva 
 |-  ( A e. _om -> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) )
51 f1fun 
 |-  ( F : ( ~P _om i^i Fin ) -1-1-> _om -> Fun F )
52 2 51 ax-mp 
 |-  Fun F
53 f1dm 
 |-  ( F : ( ~P _om i^i Fin ) -1-1-> _om -> dom F = ( ~P _om i^i Fin ) )
54 2 53 ax-mp 
 |-  dom F = ( ~P _om i^i Fin )
55 3 54 sseqtrrdi 
 |-  ( A e. _om -> ~P A C_ dom F )
56 funimass4 
 |-  ( ( Fun F /\ ~P A C_ dom F ) -> ( ( F " ~P A ) C_ ( card ` ~P A ) <-> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) ) )
57 52 55 56 sylancr 
 |-  ( A e. _om -> ( ( F " ~P A ) C_ ( card ` ~P A ) <-> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) ) )
58 50 57 mpbird 
 |-  ( A e. _om -> ( F " ~P A ) C_ ( card ` ~P A ) )
59 sspss 
 |-  ( ( F " ~P A ) C_ ( card ` ~P A ) <-> ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) )
60 58 59 sylib 
 |-  ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) )
61 orel1 
 |-  ( -. ( F " ~P A ) C. ( card ` ~P A ) -> ( ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) -> ( F " ~P A ) = ( card ` ~P A ) ) )
62 26 60 61 sylc 
 |-  ( A e. _om -> ( F " ~P A ) = ( card ` ~P A ) )