Metamath Proof Explorer

Theorem fin1a2lem6

Description: Lemma for fin1a2 . Establish that _om can be broken into two equipollent 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 fin1a2lem6 
|- ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E )

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 2 fin1a2lem2 
 |-  S : On -1-1-> On
4 1 fin1a2lem4 
 |-  E : _om -1-1-> _om
5 f1f 
 |-  ( E : _om -1-1-> _om -> E : _om --> _om )
6 frn 
 |-  ( E : _om --> _om -> ran E C_ _om )
7 omsson 
 |-  _om C_ On
8 6 7 sstrdi 
 |-  ( E : _om --> _om -> ran E C_ On )
9 4 5 8 mp2b 
 |-  ran E C_ On
10 f1ores 
 |-  ( ( S : On -1-1-> On /\ ran E C_ On ) -> ( S |` ran E ) : ran E -1-1-onto-> ( S " ran E ) )
11 3 9 10 mp2an 
 |-  ( S |` ran E ) : ran E -1-1-onto-> ( S " ran E )
12 9 sseli 
 |-  ( b e. ran E -> b e. On )
13 2 fin1a2lem1 
 |-  ( b e. On -> ( S ` b ) = suc b )
14 12 13 syl 
 |-  ( b e. ran E -> ( S ` b ) = suc b )
15 14 eqeq1d 
 |-  ( b e. ran E -> ( ( S ` b ) = a <-> suc b = a ) )
16 15 rexbiia 
 |-  ( E. b e. ran E ( S ` b ) = a <-> E. b e. ran E suc b = a )
17 4 5 6 mp2b 
 |-  ran E C_ _om
18 17 sseli 
 |-  ( b e. ran E -> b e. _om )
19 peano2 
 |-  ( b e. _om -> suc b e. _om )
20 18 19 syl 
 |-  ( b e. ran E -> suc b e. _om )
21 1 fin1a2lem5 
 |-  ( b e. _om -> ( b e. ran E <-> -. suc b e. ran E ) )
22 21 biimpd 
 |-  ( b e. _om -> ( b e. ran E -> -. suc b e. ran E ) )
23 18 22 mpcom 
 |-  ( b e. ran E -> -. suc b e. ran E )
24 20 23 jca 
 |-  ( b e. ran E -> ( suc b e. _om /\ -. suc b e. ran E ) )
25 eleq1 
 |-  ( suc b = a -> ( suc b e. _om <-> a e. _om ) )
26 eleq1 
 |-  ( suc b = a -> ( suc b e. ran E <-> a e. ran E ) )
27 26 notbid 
 |-  ( suc b = a -> ( -. suc b e. ran E <-> -. a e. ran E ) )
28 25 27 anbi12d 
 |-  ( suc b = a -> ( ( suc b e. _om /\ -. suc b e. ran E ) <-> ( a e. _om /\ -. a e. ran E ) ) )
29 24 28 syl5ibcom 
 |-  ( b e. ran E -> ( suc b = a -> ( a e. _om /\ -. a e. ran E ) ) )
30 29 rexlimiv 
 |-  ( E. b e. ran E suc b = a -> ( a e. _om /\ -. a e. ran E ) )
31 peano1 
 |-  (/) e. _om
32 1 fin1a2lem3 
 |-  ( (/) e. _om -> ( E ` (/) ) = ( 2o .o (/) ) )
33 31 32 ax-mp 
 |-  ( E ` (/) ) = ( 2o .o (/) )
34 2on 
 |-  2o e. On
35 om0 
 |-  ( 2o e. On -> ( 2o .o (/) ) = (/) )
36 34 35 ax-mp 
 |-  ( 2o .o (/) ) = (/)
37 33 36 eqtri 
 |-  ( E ` (/) ) = (/)
38 f1fun 
 |-  ( E : _om -1-1-> _om -> Fun E )
39 4 38 ax-mp 
 |-  Fun E
40 f1dm 
 |-  ( E : _om -1-1-> _om -> dom E = _om )
41 4 40 ax-mp 
 |-  dom E = _om
42 31 41 eleqtrri 
 |-  (/) e. dom E
43 fvelrn 
 |-  ( ( Fun E /\ (/) e. dom E ) -> ( E ` (/) ) e. ran E )
44 39 42 43 mp2an 
 |-  ( E ` (/) ) e. ran E
45 37 44 eqeltrri 
 |-  (/) e. ran E
46 eleq1 
 |-  ( a = (/) -> ( a e. ran E <-> (/) e. ran E ) )
47 45 46 mpbiri 
 |-  ( a = (/) -> a e. ran E )
48 47 necon3bi 
 |-  ( -. a e. ran E -> a =/= (/) )
49 nnsuc 
 |-  ( ( a e. _om /\ a =/= (/) ) -> E. b e. _om a = suc b )
50 48 49 sylan2 
 |-  ( ( a e. _om /\ -. a e. ran E ) -> E. b e. _om a = suc b )
51 eleq1 
 |-  ( a = suc b -> ( a e. _om <-> suc b e. _om ) )
52 eleq1 
 |-  ( a = suc b -> ( a e. ran E <-> suc b e. ran E ) )
53 52 notbid 
 |-  ( a = suc b -> ( -. a e. ran E <-> -. suc b e. ran E ) )
54 51 53 anbi12d 
 |-  ( a = suc b -> ( ( a e. _om /\ -. a e. ran E ) <-> ( suc b e. _om /\ -. suc b e. ran E ) ) )
55 54 anbi1d 
 |-  ( a = suc b -> ( ( ( a e. _om /\ -. a e. ran E ) /\ b e. _om ) <-> ( ( suc b e. _om /\ -. suc b e. ran E ) /\ b e. _om ) ) )
56 simplr 
 |-  ( ( ( suc b e. _om /\ -. suc b e. ran E ) /\ b e. _om ) -> -. suc b e. ran E )
57 21 adantl 
 |-  ( ( ( suc b e. _om /\ -. suc b e. ran E ) /\ b e. _om ) -> ( b e. ran E <-> -. suc b e. ran E ) )
58 56 57 mpbird 
 |-  ( ( ( suc b e. _om /\ -. suc b e. ran E ) /\ b e. _om ) -> b e. ran E )
59 55 58 syl6bi 
 |-  ( a = suc b -> ( ( ( a e. _om /\ -. a e. ran E ) /\ b e. _om ) -> b e. ran E ) )
60 59 com12 
 |-  ( ( ( a e. _om /\ -. a e. ran E ) /\ b e. _om ) -> ( a = suc b -> b e. ran E ) )
61 60 impr 
 |-  ( ( ( a e. _om /\ -. a e. ran E ) /\ ( b e. _om /\ a = suc b ) ) -> b e. ran E )
62 simprr 
 |-  ( ( ( a e. _om /\ -. a e. ran E ) /\ ( b e. _om /\ a = suc b ) ) -> a = suc b )
63 62 eqcomd 
 |-  ( ( ( a e. _om /\ -. a e. ran E ) /\ ( b e. _om /\ a = suc b ) ) -> suc b = a )
64 50 61 63 reximssdv 
 |-  ( ( a e. _om /\ -. a e. ran E ) -> E. b e. ran E suc b = a )
65 30 64 impbii 
 |-  ( E. b e. ran E suc b = a <-> ( a e. _om /\ -. a e. ran E ) )
66 16 65 bitri 
 |-  ( E. b e. ran E ( S ` b ) = a <-> ( a e. _om /\ -. a e. ran E ) )
67 f1fn 
 |-  ( S : On -1-1-> On -> S Fn On )
68 3 67 ax-mp 
 |-  S Fn On
69 fvelimab 
 |-  ( ( S Fn On /\ ran E C_ On ) -> ( a e. ( S " ran E ) <-> E. b e. ran E ( S ` b ) = a ) )
70 68 9 69 mp2an 
 |-  ( a e. ( S " ran E ) <-> E. b e. ran E ( S ` b ) = a )
71 eldif 
 |-  ( a e. ( _om \ ran E ) <-> ( a e. _om /\ -. a e. ran E ) )
72 66 70 71 3bitr4i 
 |-  ( a e. ( S " ran E ) <-> a e. ( _om \ ran E ) )
73 72 eqriv 
 |-  ( S " ran E ) = ( _om \ ran E )
74 f1oeq3 
 |-  ( ( S " ran E ) = ( _om \ ran E ) -> ( ( S |` ran E ) : ran E -1-1-onto-> ( S " ran E ) <-> ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E ) ) )
75 73 74 ax-mp 
 |-  ( ( S |` ran E ) : ran E -1-1-onto-> ( S " ran E ) <-> ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E ) )
76 11 75 mpbi 
 |-  ( S |` ran E ) : ran E -1-1-onto-> ( _om \ ran E )