Metamath Proof Explorer

Theorem ackbij1lem18

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 ackbij1lem18 
|- ( A e. ( ~P _om i^i Fin ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = 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 difss 
 |-  ( A \ |^| ( _om \ A ) ) C_ A
3 1 ackbij1lem11 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ ( A \ |^| ( _om \ A ) ) C_ A ) -> ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) )
4 2 3 mpan2 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) )
5 difss 
 |-  ( _om \ A ) C_ _om
6 omsson 
 |-  _om C_ On
7 5 6 sstri 
 |-  ( _om \ A ) C_ On
8 ominf 
 |-  -. _om e. Fin
9 elinel2 
 |-  ( A e. ( ~P _om i^i Fin ) -> A e. Fin )
10 difinf 
 |-  ( ( -. _om e. Fin /\ A e. Fin ) -> -. ( _om \ A ) e. Fin )
11 8 9 10 sylancr 
 |-  ( A e. ( ~P _om i^i Fin ) -> -. ( _om \ A ) e. Fin )
12 0fin 
 |-  (/) e. Fin
13 eleq1 
 |-  ( ( _om \ A ) = (/) -> ( ( _om \ A ) e. Fin <-> (/) e. Fin ) )
14 12 13 mpbiri 
 |-  ( ( _om \ A ) = (/) -> ( _om \ A ) e. Fin )
15 14 necon3bi 
 |-  ( -. ( _om \ A ) e. Fin -> ( _om \ A ) =/= (/) )
16 11 15 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( _om \ A ) =/= (/) )
17 onint 
 |-  ( ( ( _om \ A ) C_ On /\ ( _om \ A ) =/= (/) ) -> |^| ( _om \ A ) e. ( _om \ A ) )
18 7 16 17 sylancr 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) e. ( _om \ A ) )
19 18 eldifad 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) e. _om )
20 ackbij1lem4 
 |-  ( |^| ( _om \ A ) e. _om -> { |^| ( _om \ A ) } e. ( ~P _om i^i Fin ) )
21 19 20 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> { |^| ( _om \ A ) } e. ( ~P _om i^i Fin ) )
22 ackbij1lem6 
 |-  ( ( ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) /\ { |^| ( _om \ A ) } e. ( ~P _om i^i Fin ) ) -> ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) e. ( ~P _om i^i Fin ) )
23 4 21 22 syl2anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) e. ( ~P _om i^i Fin ) )
24 18 eldifbd 
 |-  ( A e. ( ~P _om i^i Fin ) -> -. |^| ( _om \ A ) e. A )
25 disjsn 
 |-  ( ( A i^i { |^| ( _om \ A ) } ) = (/) <-> -. |^| ( _om \ A ) e. A )
26 24 25 sylibr 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( A i^i { |^| ( _om \ A ) } ) = (/) )
27 ssdisj 
 |-  ( ( ( A \ |^| ( _om \ A ) ) C_ A /\ ( A i^i { |^| ( _om \ A ) } ) = (/) ) -> ( ( A \ |^| ( _om \ A ) ) i^i { |^| ( _om \ A ) } ) = (/) )
28 2 26 27 sylancr 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) i^i { |^| ( _om \ A ) } ) = (/) )
29 1 ackbij1lem9 
 |-  ( ( ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) /\ { |^| ( _om \ A ) } e. ( ~P _om i^i Fin ) /\ ( ( A \ |^| ( _om \ A ) ) i^i { |^| ( _om \ A ) } ) = (/) ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` { |^| ( _om \ A ) } ) ) )
30 4 21 28 29 syl3anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` { |^| ( _om \ A ) } ) ) )
31 1 ackbij1lem14 
 |-  ( |^| ( _om \ A ) e. _om -> ( F ` { |^| ( _om \ A ) } ) = suc ( F ` |^| ( _om \ A ) ) )
32 19 31 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` { |^| ( _om \ A ) } ) = suc ( F ` |^| ( _om \ A ) ) )
33 32 oveq2d 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` { |^| ( _om \ A ) } ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o suc ( F ` |^| ( _om \ A ) ) ) )
34 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
35 34 ffvelrni 
 |-  ( ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) -> ( F ` ( A \ |^| ( _om \ A ) ) ) e. _om )
36 4 35 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( A \ |^| ( _om \ A ) ) ) e. _om )
37 ackbij1lem3 
 |-  ( |^| ( _om \ A ) e. _om -> |^| ( _om \ A ) e. ( ~P _om i^i Fin ) )
38 19 37 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) e. ( ~P _om i^i Fin ) )
39 34 ffvelrni 
 |-  ( |^| ( _om \ A ) e. ( ~P _om i^i Fin ) -> ( F ` |^| ( _om \ A ) ) e. _om )
40 38 39 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` |^| ( _om \ A ) ) e. _om )
41 nnasuc 
 |-  ( ( ( F ` ( A \ |^| ( _om \ A ) ) ) e. _om /\ ( F ` |^| ( _om \ A ) ) e. _om ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o suc ( F ` |^| ( _om \ A ) ) ) = suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) )
42 36 40 41 syl2anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o suc ( F ` |^| ( _om \ A ) ) ) = suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) )
43 disjdifr 
 |-  ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = (/)
44 43 a1i 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = (/) )
45 1 ackbij1lem9 
 |-  ( ( ( A \ |^| ( _om \ A ) ) e. ( ~P _om i^i Fin ) /\ |^| ( _om \ A ) e. ( ~P _om i^i Fin ) /\ ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = (/) ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) )
46 4 38 44 45 syl3anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) )
47 uncom 
 |-  ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) = ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) )
48 onnmin 
 |-  ( ( ( _om \ A ) C_ On /\ a e. ( _om \ A ) ) -> -. a e. |^| ( _om \ A ) )
49 7 48 mpan 
 |-  ( a e. ( _om \ A ) -> -. a e. |^| ( _om \ A ) )
50 49 con2i 
 |-  ( a e. |^| ( _om \ A ) -> -. a e. ( _om \ A ) )
51 50 adantl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> -. a e. ( _om \ A ) )
52 ordom 
 |-  Ord _om
53 ordelss 
 |-  ( ( Ord _om /\ |^| ( _om \ A ) e. _om ) -> |^| ( _om \ A ) C_ _om )
54 52 19 53 sylancr 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) C_ _om )
55 54 sselda 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> a e. _om )
56 eldif 
 |-  ( a e. ( _om \ A ) <-> ( a e. _om /\ -. a e. A ) )
57 56 simplbi2 
 |-  ( a e. _om -> ( -. a e. A -> a e. ( _om \ A ) ) )
58 57 orrd 
 |-  ( a e. _om -> ( a e. A \/ a e. ( _om \ A ) ) )
59 58 orcomd 
 |-  ( a e. _om -> ( a e. ( _om \ A ) \/ a e. A ) )
60 55 59 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> ( a e. ( _om \ A ) \/ a e. A ) )
61 orel1 
 |-  ( -. a e. ( _om \ A ) -> ( ( a e. ( _om \ A ) \/ a e. A ) -> a e. A ) )
62 51 60 61 sylc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> a e. A )
63 62 ex 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( a e. |^| ( _om \ A ) -> a e. A ) )
64 63 ssrdv 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) C_ A )
65 undif 
 |-  ( |^| ( _om \ A ) C_ A <-> ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) ) = A )
66 64 65 sylib 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) ) = A )
67 47 66 eqtrid 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) = A )
68 67 fveq2d 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) ) = ( F ` A ) )
69 46 68 eqtr3d 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = ( F ` A ) )
70 suceq 
 |-  ( ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = ( F ` A ) -> suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
71 69 70 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
72 42 71 eqtrd 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o suc ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
73 30 33 72 3eqtrd 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = suc ( F ` A ) )
74 fveqeq2 
 |-  ( b = ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) -> ( ( F ` b ) = suc ( F ` A ) <-> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = suc ( F ` A ) ) )
75 74 rspcev 
 |-  ( ( ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) e. ( ~P _om i^i Fin ) /\ ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = suc ( F ` A ) ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` A ) )
76 23 73 75 syl2anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` A ) )