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 sselid
 |-  ( 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 ) )