Metamath Proof Explorer

Theorem isf32lem9

Description: Lemma for isfin3-2 . Construction of the onto function. (Contributed by Stefan O'Rear, 5-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses isf32lem.a 
|- ( ph -> F : _om --> ~P G )
isf32lem.b 
|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
isf32lem.c 
|- ( ph -> -. |^| ran F e. ran F )
isf32lem.d 
|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
isf32lem.e 
|- J = ( u e. _om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
isf32lem.f 
|- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
isf32lem.g 
|- L = ( t e. G |-> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) )
Assertion isf32lem9 
|- ( ph -> L : G -onto-> _om )

Proof

Step Hyp Ref Expression
1 isf32lem.a 
 |-  ( ph -> F : _om --> ~P G )
2 isf32lem.b 
 |-  ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3 isf32lem.c 
 |-  ( ph -> -. |^| ran F e. ran F )
4 isf32lem.d 
 |-  S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
5 isf32lem.e 
 |-  J = ( u e. _om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
6 isf32lem.f 
 |-  K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
7 isf32lem.g 
 |-  L = ( t e. G |-> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) )
8 ssab2 
 |-  { s | ( s e. _om /\ t e. ( K ` s ) ) } C_ _om
9 iotacl 
 |-  ( E! s ( s e. _om /\ t e. ( K ` s ) ) -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. { s | ( s e. _om /\ t e. ( K ` s ) ) } )
10 8 9 sselid 
 |-  ( E! s ( s e. _om /\ t e. ( K ` s ) ) -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. _om )
11 iotanul 
 |-  ( -. E! s ( s e. _om /\ t e. ( K ` s ) ) -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) = (/) )
12 peano1 
 |-  (/) e. _om
13 11 12 eqeltrdi 
 |-  ( -. E! s ( s e. _om /\ t e. ( K ` s ) ) -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. _om )
14 10 13 pm2.61i 
 |-  ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. _om
15 14 a1i 
 |-  ( t e. G -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. _om )
16 7 15 fmpti 
 |-  L : G --> _om
17 16 a1i 
 |-  ( ph -> L : G --> _om )
18 1 2 3 4 5 6 isf32lem6 
 |-  ( ( ph /\ a e. _om ) -> ( K ` a ) =/= (/) )
19 n0 
 |-  ( ( K ` a ) =/= (/) <-> E. b b e. ( K ` a ) )
20 18 19 sylib 
 |-  ( ( ph /\ a e. _om ) -> E. b b e. ( K ` a ) )
21 1 2 3 4 5 6 isf32lem8 
 |-  ( ( ph /\ a e. _om ) -> ( K ` a ) C_ G )
22 21 sselda 
 |-  ( ( ( ph /\ a e. _om ) /\ b e. ( K ` a ) ) -> b e. G )
23 eleq1w 
 |-  ( t = b -> ( t e. ( K ` s ) <-> b e. ( K ` s ) ) )
24 23 anbi2d 
 |-  ( t = b -> ( ( s e. _om /\ t e. ( K ` s ) ) <-> ( s e. _om /\ b e. ( K ` s ) ) ) )
25 24 iotabidv 
 |-  ( t = b -> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) = ( iota s ( s e. _om /\ b e. ( K ` s ) ) ) )
26 iotaex 
 |-  ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) e. _V
27 25 7 26 fvmpt3i 
 |-  ( b e. G -> ( L ` b ) = ( iota s ( s e. _om /\ b e. ( K ` s ) ) ) )
28 22 27 syl 
 |-  ( ( ( ph /\ a e. _om ) /\ b e. ( K ` a ) ) -> ( L ` b ) = ( iota s ( s e. _om /\ b e. ( K ` s ) ) ) )
29 simp1r 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om /\ s e. _om ) -> b e. ( K ` a ) )
30 simpl1 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> ph )
31 simpr 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> s =/= a )
32 31 necomd 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> a =/= s )
33 simpl2 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> a e. _om )
34 simpl3 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> s e. _om )
35 1 2 3 4 5 6 isf32lem7 
 |-  ( ( ( ph /\ a =/= s ) /\ ( a e. _om /\ s e. _om ) ) -> ( ( K ` a ) i^i ( K ` s ) ) = (/) )
36 30 32 33 34 35 syl22anc 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> ( ( K ` a ) i^i ( K ` s ) ) = (/) )
37 disj1 
 |-  ( ( ( K ` a ) i^i ( K ` s ) ) = (/) <-> A. b ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) )
38 36 37 sylib 
 |-  ( ( ( ph /\ a e. _om /\ s e. _om ) /\ s =/= a ) -> A. b ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) )
39 38 ex 
 |-  ( ( ph /\ a e. _om /\ s e. _om ) -> ( s =/= a -> A. b ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) ) )
40 sp 
 |-  ( A. b ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) -> ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) )
41 39 40 syl6 
 |-  ( ( ph /\ a e. _om /\ s e. _om ) -> ( s =/= a -> ( b e. ( K ` a ) -> -. b e. ( K ` s ) ) ) )
42 41 com23 
 |-  ( ( ph /\ a e. _om /\ s e. _om ) -> ( b e. ( K ` a ) -> ( s =/= a -> -. b e. ( K ` s ) ) ) )
43 42 3adant1r 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om /\ s e. _om ) -> ( b e. ( K ` a ) -> ( s =/= a -> -. b e. ( K ` s ) ) ) )
44 29 43 mpd 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om /\ s e. _om ) -> ( s =/= a -> -. b e. ( K ` s ) ) )
45 44 necon4ad 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om /\ s e. _om ) -> ( b e. ( K ` s ) -> s = a ) )
46 45 3expia 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om ) -> ( s e. _om -> ( b e. ( K ` s ) -> s = a ) ) )
47 46 impd 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om ) -> ( ( s e. _om /\ b e. ( K ` s ) ) -> s = a ) )
48 eleq1w 
 |-  ( s = a -> ( s e. _om <-> a e. _om ) )
49 fveq2 
 |-  ( s = a -> ( K ` s ) = ( K ` a ) )
50 49 eleq2d 
 |-  ( s = a -> ( b e. ( K ` s ) <-> b e. ( K ` a ) ) )
51 48 50 anbi12d 
 |-  ( s = a -> ( ( s e. _om /\ b e. ( K ` s ) ) <-> ( a e. _om /\ b e. ( K ` a ) ) ) )
52 51 biimprcd 
 |-  ( ( a e. _om /\ b e. ( K ` a ) ) -> ( s = a -> ( s e. _om /\ b e. ( K ` s ) ) ) )
53 52 ancoms 
 |-  ( ( b e. ( K ` a ) /\ a e. _om ) -> ( s = a -> ( s e. _om /\ b e. ( K ` s ) ) ) )
54 53 adantll 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om ) -> ( s = a -> ( s e. _om /\ b e. ( K ` s ) ) ) )
55 47 54 impbid 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om ) -> ( ( s e. _om /\ b e. ( K ` s ) ) <-> s = a ) )
56 55 iota5 
 |-  ( ( ( ph /\ b e. ( K ` a ) ) /\ a e. _om ) -> ( iota s ( s e. _om /\ b e. ( K ` s ) ) ) = a )
57 56 an32s 
 |-  ( ( ( ph /\ a e. _om ) /\ b e. ( K ` a ) ) -> ( iota s ( s e. _om /\ b e. ( K ` s ) ) ) = a )
58 28 57 eqtr2d 
 |-  ( ( ( ph /\ a e. _om ) /\ b e. ( K ` a ) ) -> a = ( L ` b ) )
59 22 58 jca 
 |-  ( ( ( ph /\ a e. _om ) /\ b e. ( K ` a ) ) -> ( b e. G /\ a = ( L ` b ) ) )
60 59 ex 
 |-  ( ( ph /\ a e. _om ) -> ( b e. ( K ` a ) -> ( b e. G /\ a = ( L ` b ) ) ) )
61 60 eximdv 
 |-  ( ( ph /\ a e. _om ) -> ( E. b b e. ( K ` a ) -> E. b ( b e. G /\ a = ( L ` b ) ) ) )
62 df-rex 
 |-  ( E. b e. G a = ( L ` b ) <-> E. b ( b e. G /\ a = ( L ` b ) ) )
63 61 62 imbitrrdi 
 |-  ( ( ph /\ a e. _om ) -> ( E. b b e. ( K ` a ) -> E. b e. G a = ( L ` b ) ) )
64 20 63 mpd 
 |-  ( ( ph /\ a e. _om ) -> E. b e. G a = ( L ` b ) )
65 64 ralrimiva 
 |-  ( ph -> A. a e. _om E. b e. G a = ( L ` b ) )
66 dffo3 
 |-  ( L : G -onto-> _om <-> ( L : G --> _om /\ A. a e. _om E. b e. G a = ( L ` b ) ) )
67 17 65 66 sylanbrc 
 |-  ( ph -> L : G -onto-> _om )