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 incom 
 |-  ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = ( |^| ( _om \ A ) i^i ( A \ |^| ( _om \ A ) ) )
44 disjdif 
 |-  ( |^| ( _om \ A ) i^i ( A \ |^| ( _om \ A ) ) ) = (/)
45 43 44 eqtri 
 |-  ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = (/)
46 45 a1i 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) i^i |^| ( _om \ A ) ) = (/) )
47 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 ) ) ) )
48 4 38 46 47 syl3anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) ) = ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) )
49 uncom 
 |-  ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) = ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) )
50 onnmin 
 |-  ( ( ( _om \ A ) C_ On /\ a e. ( _om \ A ) ) -> -. a e. |^| ( _om \ A ) )
51 7 50 mpan 
 |-  ( a e. ( _om \ A ) -> -. a e. |^| ( _om \ A ) )
52 51 con2i 
 |-  ( a e. |^| ( _om \ A ) -> -. a e. ( _om \ A ) )
53 52 adantl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> -. a e. ( _om \ A ) )
54 ordom 
 |-  Ord _om
55 ordelss 
 |-  ( ( Ord _om /\ |^| ( _om \ A ) e. _om ) -> |^| ( _om \ A ) C_ _om )
56 54 19 55 sylancr 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) C_ _om )
57 56 sselda 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> a e. _om )
58 eldif 
 |-  ( a e. ( _om \ A ) <-> ( a e. _om /\ -. a e. A ) )
59 58 simplbi2 
 |-  ( a e. _om -> ( -. a e. A -> a e. ( _om \ A ) ) )
60 59 orrd 
 |-  ( a e. _om -> ( a e. A \/ a e. ( _om \ A ) ) )
61 60 orcomd 
 |-  ( a e. _om -> ( a e. ( _om \ A ) \/ a e. A ) )
62 57 61 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> ( a e. ( _om \ A ) \/ a e. A ) )
63 orel1 
 |-  ( -. a e. ( _om \ A ) -> ( ( a e. ( _om \ A ) \/ a e. A ) -> a e. A ) )
64 53 62 63 sylc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ a e. |^| ( _om \ A ) ) -> a e. A )
65 64 ex 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( a e. |^| ( _om \ A ) -> a e. A ) )
66 65 ssrdv 
 |-  ( A e. ( ~P _om i^i Fin ) -> |^| ( _om \ A ) C_ A )
67 undif 
 |-  ( |^| ( _om \ A ) C_ A <-> ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) ) = A )
68 66 67 sylib 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( |^| ( _om \ A ) u. ( A \ |^| ( _om \ A ) ) ) = A )
69 49 68 syl5eq 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) = A )
70 69 fveq2d 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. |^| ( _om \ A ) ) ) = ( F ` A ) )
71 48 70 eqtr3d 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = ( F ` A ) )
72 suceq 
 |-  ( ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = ( F ` A ) -> suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
73 71 72 syl 
 |-  ( A e. ( ~P _om i^i Fin ) -> suc ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
74 42 73 eqtrd 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( ( F ` ( A \ |^| ( _om \ A ) ) ) +o suc ( F ` |^| ( _om \ A ) ) ) = suc ( F ` A ) )
75 30 33 74 3eqtrd 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = suc ( F ` A ) )
76 fveqeq2 
 |-  ( b = ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) -> ( ( F ` b ) = suc ( F ` A ) <-> ( F ` ( ( A \ |^| ( _om \ A ) ) u. { |^| ( _om \ A ) } ) ) = suc ( F ` A ) ) )
77 76 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 ) )
78 23 75 77 syl2anc 
 |-  ( A e. ( ~P _om i^i Fin ) -> E. b e. ( ~P _om i^i Fin ) ( F ` b ) = suc ( F ` A ) )