Metamath Proof Explorer

Theorem fin1a2lem7

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypotheses fin1a2lem.b 
|- E = ( x e. _om |-> ( 2o .o x ) )
fin1a2lem.aa 
|- S = ( x e. On |-> suc x )
Assertion fin1a2lem7 
|- ( ( A e. V /\ A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) ) -> A e. Fin3 )

Proof

Step Hyp Ref Expression
1 fin1a2lem.b 
 |-  E = ( x e. _om |-> ( 2o .o x ) )
2 fin1a2lem.aa 
 |-  S = ( x e. On |-> suc x )
3 peano1 
 |-  (/) e. _om
4 ne0i 
 |-  ( (/) e. _om -> _om =/= (/) )
5 brwdomn0 
 |-  ( _om =/= (/) -> ( _om ~<_* A <-> E. f f : A -onto-> _om ) )
6 3 4 5 mp2b 
 |-  ( _om ~<_* A <-> E. f f : A -onto-> _om )
7 vex 
 |-  f e. _V
8 fof 
 |-  ( f : A -onto-> _om -> f : A --> _om )
9 dmfex 
 |-  ( ( f e. _V /\ f : A --> _om ) -> A e. _V )
10 7 8 9 sylancr 
 |-  ( f : A -onto-> _om -> A e. _V )
11 cnvimass 
 |-  ( `' f " ran E ) C_ dom f
12 11 8 fssdm 
 |-  ( f : A -onto-> _om -> ( `' f " ran E ) C_ A )
13 10 12 sselpwd 
 |-  ( f : A -onto-> _om -> ( `' f " ran E ) e. ~P A )
14 1 fin1a2lem4 
 |-  E : _om -1-1-> _om
15 f1cnv 
 |-  ( E : _om -1-1-> _om -> `' E : ran E -1-1-onto-> _om )
16 f1ofo 
 |-  ( `' E : ran E -1-1-onto-> _om -> `' E : ran E -onto-> _om )
17 14 15 16 mp2b 
 |-  `' E : ran E -onto-> _om
18 fofun 
 |-  ( `' E : ran E -onto-> _om -> Fun `' E )
19 17 18 ax-mp 
 |-  Fun `' E
20 7 resex 
 |-  ( f |` ( `' f " ran E ) ) e. _V
21 cofunexg 
 |-  ( ( Fun `' E /\ ( f |` ( `' f " ran E ) ) e. _V ) -> ( `' E o. ( f |` ( `' f " ran E ) ) ) e. _V )
22 19 20 21 mp2an 
 |-  ( `' E o. ( f |` ( `' f " ran E ) ) ) e. _V
23 fofun 
 |-  ( f : A -onto-> _om -> Fun f )
24 fores 
 |-  ( ( Fun f /\ ( `' f " ran E ) C_ dom f ) -> ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ( f " ( `' f " ran E ) ) )
25 23 11 24 sylancl 
 |-  ( f : A -onto-> _om -> ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ( f " ( `' f " ran E ) ) )
26 f1f 
 |-  ( E : _om -1-1-> _om -> E : _om --> _om )
27 frn 
 |-  ( E : _om --> _om -> ran E C_ _om )
28 14 26 27 mp2b 
 |-  ran E C_ _om
29 foimacnv 
 |-  ( ( f : A -onto-> _om /\ ran E C_ _om ) -> ( f " ( `' f " ran E ) ) = ran E )
30 28 29 mpan2 
 |-  ( f : A -onto-> _om -> ( f " ( `' f " ran E ) ) = ran E )
31 foeq3 
 |-  ( ( f " ( `' f " ran E ) ) = ran E -> ( ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ( f " ( `' f " ran E ) ) <-> ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ran E ) )
32 30 31 syl 
 |-  ( f : A -onto-> _om -> ( ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ( f " ( `' f " ran E ) ) <-> ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ran E ) )
33 25 32 mpbid 
 |-  ( f : A -onto-> _om -> ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ran E )
34 foco 
 |-  ( ( `' E : ran E -onto-> _om /\ ( f |` ( `' f " ran E ) ) : ( `' f " ran E ) -onto-> ran E ) -> ( `' E o. ( f |` ( `' f " ran E ) ) ) : ( `' f " ran E ) -onto-> _om )
35 17 33 34 sylancr 
 |-  ( f : A -onto-> _om -> ( `' E o. ( f |` ( `' f " ran E ) ) ) : ( `' f " ran E ) -onto-> _om )
36 fowdom 
 |-  ( ( ( `' E o. ( f |` ( `' f " ran E ) ) ) e. _V /\ ( `' E o. ( f |` ( `' f " ran E ) ) ) : ( `' f " ran E ) -onto-> _om ) -> _om ~<_* ( `' f " ran E ) )
37 22 35 36 sylancr 
 |-  ( f : A -onto-> _om -> _om ~<_* ( `' f " ran E ) )
38 7 cnvex 
 |-  `' f e. _V
39 38 imaex 
 |-  ( `' f " ran E ) e. _V
40 isfin3-2 
 |-  ( ( `' f " ran E ) e. _V -> ( ( `' f " ran E ) e. Fin3 <-> -. _om ~<_* ( `' f " ran E ) ) )
41 39 40 ax-mp 
 |-  ( ( `' f " ran E ) e. Fin3 <-> -. _om ~<_* ( `' f " ran E ) )
42 41 con2bii 
 |-  ( _om ~<_* ( `' f " ran E ) <-> -. ( `' f " ran E ) e. Fin3 )
43 37 42 sylib 
 |-  ( f : A -onto-> _om -> -. ( `' f " ran E ) e. Fin3 )
44 1 2 fin1a2lem6 
 |-  ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E )
45 f1ocnv 
 |-  ( ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E ) -> `' ( S |` ran E ) : ( _om \ ran E ) -1-1-onto-> ran E )
46 f1ofo 
 |-  ( `' ( S |` ran E ) : ( _om \ ran E ) -1-1-onto-> ran E -> `' ( S |` ran E ) : ( _om \ ran E ) -onto-> ran E )
47 44 45 46 mp2b 
 |-  `' ( S |` ran E ) : ( _om \ ran E ) -onto-> ran E
48 foco 
 |-  ( ( `' E : ran E -onto-> _om /\ `' ( S |` ran E ) : ( _om \ ran E ) -onto-> ran E ) -> ( `' E o. `' ( S |` ran E ) ) : ( _om \ ran E ) -onto-> _om )
49 17 47 48 mp2an 
 |-  ( `' E o. `' ( S |` ran E ) ) : ( _om \ ran E ) -onto-> _om
50 fofun 
 |-  ( ( `' E o. `' ( S |` ran E ) ) : ( _om \ ran E ) -onto-> _om -> Fun ( `' E o. `' ( S |` ran E ) ) )
51 49 50 ax-mp 
 |-  Fun ( `' E o. `' ( S |` ran E ) )
52 7 resex 
 |-  ( f |` ( A \ ( `' f " ran E ) ) ) e. _V
53 cofunexg 
 |-  ( ( Fun ( `' E o. `' ( S |` ran E ) ) /\ ( f |` ( A \ ( `' f " ran E ) ) ) e. _V ) -> ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) e. _V )
54 51 52 53 mp2an 
 |-  ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) e. _V
55 difss 
 |-  ( A \ ( `' f " ran E ) ) C_ A
56 8 fdmd 
 |-  ( f : A -onto-> _om -> dom f = A )
57 55 56 sseqtrrid 
 |-  ( f : A -onto-> _om -> ( A \ ( `' f " ran E ) ) C_ dom f )
58 fores 
 |-  ( ( Fun f /\ ( A \ ( `' f " ran E ) ) C_ dom f ) -> ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( f " ( A \ ( `' f " ran E ) ) ) )
59 23 57 58 syl2anc 
 |-  ( f : A -onto-> _om -> ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( f " ( A \ ( `' f " ran E ) ) ) )
60 funcnvcnv 
 |-  ( Fun f -> Fun `' `' f )
61 imadif 
 |-  ( Fun `' `' f -> ( `' f " ( _om \ ran E ) ) = ( ( `' f " _om ) \ ( `' f " ran E ) ) )
62 23 60 61 3syl 
 |-  ( f : A -onto-> _om -> ( `' f " ( _om \ ran E ) ) = ( ( `' f " _om ) \ ( `' f " ran E ) ) )
63 62 imaeq2d 
 |-  ( f : A -onto-> _om -> ( f " ( `' f " ( _om \ ran E ) ) ) = ( f " ( ( `' f " _om ) \ ( `' f " ran E ) ) ) )
64 difss 
 |-  ( _om \ ran E ) C_ _om
65 foimacnv 
 |-  ( ( f : A -onto-> _om /\ ( _om \ ran E ) C_ _om ) -> ( f " ( `' f " ( _om \ ran E ) ) ) = ( _om \ ran E ) )
66 64 65 mpan2 
 |-  ( f : A -onto-> _om -> ( f " ( `' f " ( _om \ ran E ) ) ) = ( _om \ ran E ) )
67 fimacnv 
 |-  ( f : A --> _om -> ( `' f " _om ) = A )
68 8 67 syl 
 |-  ( f : A -onto-> _om -> ( `' f " _om ) = A )
69 68 difeq1d 
 |-  ( f : A -onto-> _om -> ( ( `' f " _om ) \ ( `' f " ran E ) ) = ( A \ ( `' f " ran E ) ) )
70 69 imaeq2d 
 |-  ( f : A -onto-> _om -> ( f " ( ( `' f " _om ) \ ( `' f " ran E ) ) ) = ( f " ( A \ ( `' f " ran E ) ) ) )
71 63 66 70 3eqtr3rd 
 |-  ( f : A -onto-> _om -> ( f " ( A \ ( `' f " ran E ) ) ) = ( _om \ ran E ) )
72 foeq3 
 |-  ( ( f " ( A \ ( `' f " ran E ) ) ) = ( _om \ ran E ) -> ( ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( f " ( A \ ( `' f " ran E ) ) ) <-> ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( _om \ ran E ) ) )
73 71 72 syl 
 |-  ( f : A -onto-> _om -> ( ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( f " ( A \ ( `' f " ran E ) ) ) <-> ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( _om \ ran E ) ) )
74 59 73 mpbid 
 |-  ( f : A -onto-> _om -> ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( _om \ ran E ) )
75 foco 
 |-  ( ( ( `' E o. `' ( S |` ran E ) ) : ( _om \ ran E ) -onto-> _om /\ ( f |` ( A \ ( `' f " ran E ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> ( _om \ ran E ) ) -> ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> _om )
76 49 74 75 sylancr 
 |-  ( f : A -onto-> _om -> ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> _om )
77 fowdom 
 |-  ( ( ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) e. _V /\ ( ( `' E o. `' ( S |` ran E ) ) o. ( f |` ( A \ ( `' f " ran E ) ) ) ) : ( A \ ( `' f " ran E ) ) -onto-> _om ) -> _om ~<_* ( A \ ( `' f " ran E ) ) )
78 54 76 77 sylancr 
 |-  ( f : A -onto-> _om -> _om ~<_* ( A \ ( `' f " ran E ) ) )
79 difexg 
 |-  ( A e. _V -> ( A \ ( `' f " ran E ) ) e. _V )
80 isfin3-2 
 |-  ( ( A \ ( `' f " ran E ) ) e. _V -> ( ( A \ ( `' f " ran E ) ) e. Fin3 <-> -. _om ~<_* ( A \ ( `' f " ran E ) ) ) )
81 10 79 80 3syl 
 |-  ( f : A -onto-> _om -> ( ( A \ ( `' f " ran E ) ) e. Fin3 <-> -. _om ~<_* ( A \ ( `' f " ran E ) ) ) )
82 81 con2bid 
 |-  ( f : A -onto-> _om -> ( _om ~<_* ( A \ ( `' f " ran E ) ) <-> -. ( A \ ( `' f " ran E ) ) e. Fin3 ) )
83 78 82 mpbid 
 |-  ( f : A -onto-> _om -> -. ( A \ ( `' f " ran E ) ) e. Fin3 )
84 eleq1 
 |-  ( y = ( `' f " ran E ) -> ( y e. Fin3 <-> ( `' f " ran E ) e. Fin3 ) )
85 difeq2 
 |-  ( y = ( `' f " ran E ) -> ( A \ y ) = ( A \ ( `' f " ran E ) ) )
86 85 eleq1d 
 |-  ( y = ( `' f " ran E ) -> ( ( A \ y ) e. Fin3 <-> ( A \ ( `' f " ran E ) ) e. Fin3 ) )
87 84 86 orbi12d 
 |-  ( y = ( `' f " ran E ) -> ( ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) <-> ( ( `' f " ran E ) e. Fin3 \/ ( A \ ( `' f " ran E ) ) e. Fin3 ) ) )
88 87 notbid 
 |-  ( y = ( `' f " ran E ) -> ( -. ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) <-> -. ( ( `' f " ran E ) e. Fin3 \/ ( A \ ( `' f " ran E ) ) e. Fin3 ) ) )
89 ioran 
 |-  ( -. ( ( `' f " ran E ) e. Fin3 \/ ( A \ ( `' f " ran E ) ) e. Fin3 ) <-> ( -. ( `' f " ran E ) e. Fin3 /\ -. ( A \ ( `' f " ran E ) ) e. Fin3 ) )
90 88 89 bitrdi 
 |-  ( y = ( `' f " ran E ) -> ( -. ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) <-> ( -. ( `' f " ran E ) e. Fin3 /\ -. ( A \ ( `' f " ran E ) ) e. Fin3 ) ) )
91 90 rspcev 
 |-  ( ( ( `' f " ran E ) e. ~P A /\ ( -. ( `' f " ran E ) e. Fin3 /\ -. ( A \ ( `' f " ran E ) ) e. Fin3 ) ) -> E. y e. ~P A -. ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
92 13 43 83 91 syl12anc 
 |-  ( f : A -onto-> _om -> E. y e. ~P A -. ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
93 rexnal 
 |-  ( E. y e. ~P A -. ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) <-> -. A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
94 92 93 sylib 
 |-  ( f : A -onto-> _om -> -. A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
95 94 exlimiv 
 |-  ( E. f f : A -onto-> _om -> -. A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
96 6 95 sylbi 
 |-  ( _om ~<_* A -> -. A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) )
97 96 con2i 
 |-  ( A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) -> -. _om ~<_* A )
98 isfin3-2 
 |-  ( A e. V -> ( A e. Fin3 <-> -. _om ~<_* A ) )
99 97 98 syl5ibr 
 |-  ( A e. V -> ( A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) -> A e. Fin3 ) )
100 99 imp 
 |-  ( ( A e. V /\ A. y e. ~P A ( y e. Fin3 \/ ( A \ y ) e. Fin3 ) ) -> A e. Fin3 )