Metamath Proof Explorer

Theorem ackbij1lem14

Description: Lemma for ackbij1 . (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 ackbij1lem14 
|- ( A e. _om -> ( F ` { A } ) = suc ( F ` 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 ackbij1lem8 
 |-  ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) )
3 pweq 
 |-  ( a = (/) -> ~P a = ~P (/) )
4 3 fveq2d 
 |-  ( a = (/) -> ( card ` ~P a ) = ( card ` ~P (/) ) )
5 fveq2 
 |-  ( a = (/) -> ( F ` a ) = ( F ` (/) ) )
6 suceq 
 |-  ( ( F ` a ) = ( F ` (/) ) -> suc ( F ` a ) = suc ( F ` (/) ) )
7 5 6 syl 
 |-  ( a = (/) -> suc ( F ` a ) = suc ( F ` (/) ) )
8 4 7 eqeq12d 
 |-  ( a = (/) -> ( ( card ` ~P a ) = suc ( F ` a ) <-> ( card ` ~P (/) ) = suc ( F ` (/) ) ) )
9 pweq 
 |-  ( a = b -> ~P a = ~P b )
10 9 fveq2d 
 |-  ( a = b -> ( card ` ~P a ) = ( card ` ~P b ) )
11 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
12 suceq 
 |-  ( ( F ` a ) = ( F ` b ) -> suc ( F ` a ) = suc ( F ` b ) )
13 11 12 syl 
 |-  ( a = b -> suc ( F ` a ) = suc ( F ` b ) )
14 10 13 eqeq12d 
 |-  ( a = b -> ( ( card ` ~P a ) = suc ( F ` a ) <-> ( card ` ~P b ) = suc ( F ` b ) ) )
15 pweq 
 |-  ( a = suc b -> ~P a = ~P suc b )
16 15 fveq2d 
 |-  ( a = suc b -> ( card ` ~P a ) = ( card ` ~P suc b ) )
17 fveq2 
 |-  ( a = suc b -> ( F ` a ) = ( F ` suc b ) )
18 suceq 
 |-  ( ( F ` a ) = ( F ` suc b ) -> suc ( F ` a ) = suc ( F ` suc b ) )
19 17 18 syl 
 |-  ( a = suc b -> suc ( F ` a ) = suc ( F ` suc b ) )
20 16 19 eqeq12d 
 |-  ( a = suc b -> ( ( card ` ~P a ) = suc ( F ` a ) <-> ( card ` ~P suc b ) = suc ( F ` suc b ) ) )
21 pweq 
 |-  ( a = A -> ~P a = ~P A )
22 21 fveq2d 
 |-  ( a = A -> ( card ` ~P a ) = ( card ` ~P A ) )
23 fveq2 
 |-  ( a = A -> ( F ` a ) = ( F ` A ) )
24 suceq 
 |-  ( ( F ` a ) = ( F ` A ) -> suc ( F ` a ) = suc ( F ` A ) )
25 23 24 syl 
 |-  ( a = A -> suc ( F ` a ) = suc ( F ` A ) )
26 22 25 eqeq12d 
 |-  ( a = A -> ( ( card ` ~P a ) = suc ( F ` a ) <-> ( card ` ~P A ) = suc ( F ` A ) ) )
27 df-1o 
 |-  1o = suc (/)
28 pw0 
 |-  ~P (/) = { (/) }
29 28 fveq2i 
 |-  ( card ` ~P (/) ) = ( card ` { (/) } )
30 0ex 
 |-  (/) e. _V
31 cardsn 
 |-  ( (/) e. _V -> ( card ` { (/) } ) = 1o )
32 30 31 ax-mp 
 |-  ( card ` { (/) } ) = 1o
33 29 32 eqtri 
 |-  ( card ` ~P (/) ) = 1o
34 1 ackbij1lem13 
 |-  ( F ` (/) ) = (/)
35 suceq 
 |-  ( ( F ` (/) ) = (/) -> suc ( F ` (/) ) = suc (/) )
36 34 35 ax-mp 
 |-  suc ( F ` (/) ) = suc (/)
37 27 33 36 3eqtr4i 
 |-  ( card ` ~P (/) ) = suc ( F ` (/) )
38 oveq2 
 |-  ( ( card ` ~P b ) = suc ( F ` b ) -> ( ( card ` ~P b ) +o ( card ` ~P b ) ) = ( ( card ` ~P b ) +o suc ( F ` b ) ) )
39 38 adantl 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( ( card ` ~P b ) +o ( card ` ~P b ) ) = ( ( card ` ~P b ) +o suc ( F ` b ) ) )
40 ackbij1lem5 
 |-  ( b e. _om -> ( card ` ~P suc b ) = ( ( card ` ~P b ) +o ( card ` ~P b ) ) )
41 40 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( card ` ~P suc b ) = ( ( card ` ~P b ) +o ( card ` ~P b ) ) )
42 df-suc 
 |-  suc b = ( b u. { b } )
43 42 equncomi 
 |-  suc b = ( { b } u. b )
44 43 fveq2i 
 |-  ( F ` suc b ) = ( F ` ( { b } u. b ) )
45 ackbij1lem4 
 |-  ( b e. _om -> { b } e. ( ~P _om i^i Fin ) )
46 45 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> { b } e. ( ~P _om i^i Fin ) )
47 ackbij1lem3 
 |-  ( b e. _om -> b e. ( ~P _om i^i Fin ) )
48 47 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> b e. ( ~P _om i^i Fin ) )
49 incom 
 |-  ( { b } i^i b ) = ( b i^i { b } )
50 nnord 
 |-  ( b e. _om -> Ord b )
51 orddisj 
 |-  ( Ord b -> ( b i^i { b } ) = (/) )
52 50 51 syl 
 |-  ( b e. _om -> ( b i^i { b } ) = (/) )
53 49 52 eqtrid 
 |-  ( b e. _om -> ( { b } i^i b ) = (/) )
54 53 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( { b } i^i b ) = (/) )
55 1 ackbij1lem9 
 |-  ( ( { b } e. ( ~P _om i^i Fin ) /\ b e. ( ~P _om i^i Fin ) /\ ( { b } i^i b ) = (/) ) -> ( F ` ( { b } u. b ) ) = ( ( F ` { b } ) +o ( F ` b ) ) )
56 46 48 54 55 syl3anc 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( F ` ( { b } u. b ) ) = ( ( F ` { b } ) +o ( F ` b ) ) )
57 1 ackbij1lem8 
 |-  ( b e. _om -> ( F ` { b } ) = ( card ` ~P b ) )
58 57 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( F ` { b } ) = ( card ` ~P b ) )
59 58 oveq1d 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( ( F ` { b } ) +o ( F ` b ) ) = ( ( card ` ~P b ) +o ( F ` b ) ) )
60 56 59 eqtrd 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( F ` ( { b } u. b ) ) = ( ( card ` ~P b ) +o ( F ` b ) ) )
61 44 60 eqtrid 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( F ` suc b ) = ( ( card ` ~P b ) +o ( F ` b ) ) )
62 suceq 
 |-  ( ( F ` suc b ) = ( ( card ` ~P b ) +o ( F ` b ) ) -> suc ( F ` suc b ) = suc ( ( card ` ~P b ) +o ( F ` b ) ) )
63 61 62 syl 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> suc ( F ` suc b ) = suc ( ( card ` ~P b ) +o ( F ` b ) ) )
64 nnfi 
 |-  ( b e. _om -> b e. Fin )
65 pwfi 
 |-  ( b e. Fin <-> ~P b e. Fin )
66 64 65 sylib 
 |-  ( b e. _om -> ~P b e. Fin )
67 66 adantr 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ~P b e. Fin )
68 ficardom 
 |-  ( ~P b e. Fin -> ( card ` ~P b ) e. _om )
69 67 68 syl 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( card ` ~P b ) e. _om )
70 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
71 70 ffvelrni 
 |-  ( b e. ( ~P _om i^i Fin ) -> ( F ` b ) e. _om )
72 48 71 syl 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( F ` b ) e. _om )
73 nnasuc 
 |-  ( ( ( card ` ~P b ) e. _om /\ ( F ` b ) e. _om ) -> ( ( card ` ~P b ) +o suc ( F ` b ) ) = suc ( ( card ` ~P b ) +o ( F ` b ) ) )
74 69 72 73 syl2anc 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( ( card ` ~P b ) +o suc ( F ` b ) ) = suc ( ( card ` ~P b ) +o ( F ` b ) ) )
75 63 74 eqtr4d 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> suc ( F ` suc b ) = ( ( card ` ~P b ) +o suc ( F ` b ) ) )
76 39 41 75 3eqtr4d 
 |-  ( ( b e. _om /\ ( card ` ~P b ) = suc ( F ` b ) ) -> ( card ` ~P suc b ) = suc ( F ` suc b ) )
77 76 ex 
 |-  ( b e. _om -> ( ( card ` ~P b ) = suc ( F ` b ) -> ( card ` ~P suc b ) = suc ( F ` suc b ) ) )
78 8 14 20 26 37 77 finds 
 |-  ( A e. _om -> ( card ` ~P A ) = suc ( F ` A ) )
79 2 78 eqtrd 
 |-  ( A e. _om -> ( F ` { A } ) = suc ( F ` A ) )