Metamath Proof Explorer

Theorem infpssrlem5

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Hypotheses infpssrlem.a 
|- ( ph -> B C_ A )
infpssrlem.c 
|- ( ph -> F : B -1-1-onto-> A )
infpssrlem.d 
|- ( ph -> C e. ( A \ B ) )
infpssrlem.e 
|- G = ( rec ( `' F , C ) |` _om )
Assertion infpssrlem5 
|- ( ph -> ( A e. V -> _om ~<_ A ) )

Proof

Step Hyp Ref Expression
1 infpssrlem.a 
 |-  ( ph -> B C_ A )
2 infpssrlem.c 
 |-  ( ph -> F : B -1-1-onto-> A )
3 infpssrlem.d 
 |-  ( ph -> C e. ( A \ B ) )
4 infpssrlem.e 
 |-  G = ( rec ( `' F , C ) |` _om )
5 1 2 3 4 infpssrlem3 
 |-  ( ph -> G : _om --> A )
6 simpll 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ b e. c ) -> ph )
7 simplrr 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ b e. c ) -> c e. _om )
8 simpr 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ b e. c ) -> b e. c )
9 1 2 3 4 infpssrlem4 
 |-  ( ( ph /\ c e. _om /\ b e. c ) -> ( G ` c ) =/= ( G ` b ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ b e. c ) -> ( G ` c ) =/= ( G ` b ) )
11 10 necomd 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ b e. c ) -> ( G ` b ) =/= ( G ` c ) )
12 simpll 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ c e. b ) -> ph )
13 simplrl 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ c e. b ) -> b e. _om )
14 simpr 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ c e. b ) -> c e. b )
15 1 2 3 4 infpssrlem4 
 |-  ( ( ph /\ b e. _om /\ c e. b ) -> ( G ` b ) =/= ( G ` c ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ c e. b ) -> ( G ` b ) =/= ( G ` c ) )
17 11 16 jaodan 
 |-  ( ( ( ph /\ ( b e. _om /\ c e. _om ) ) /\ ( b e. c \/ c e. b ) ) -> ( G ` b ) =/= ( G ` c ) )
18 17 ex 
 |-  ( ( ph /\ ( b e. _om /\ c e. _om ) ) -> ( ( b e. c \/ c e. b ) -> ( G ` b ) =/= ( G ` c ) ) )
19 18 necon2bd 
 |-  ( ( ph /\ ( b e. _om /\ c e. _om ) ) -> ( ( G ` b ) = ( G ` c ) -> -. ( b e. c \/ c e. b ) ) )
20 nnord 
 |-  ( b e. _om -> Ord b )
21 nnord 
 |-  ( c e. _om -> Ord c )
22 ordtri3 
 |-  ( ( Ord b /\ Ord c ) -> ( b = c <-> -. ( b e. c \/ c e. b ) ) )
23 20 21 22 syl2an 
 |-  ( ( b e. _om /\ c e. _om ) -> ( b = c <-> -. ( b e. c \/ c e. b ) ) )
24 23 adantl 
 |-  ( ( ph /\ ( b e. _om /\ c e. _om ) ) -> ( b = c <-> -. ( b e. c \/ c e. b ) ) )
25 19 24 sylibrd 
 |-  ( ( ph /\ ( b e. _om /\ c e. _om ) ) -> ( ( G ` b ) = ( G ` c ) -> b = c ) )
26 25 ralrimivva 
 |-  ( ph -> A. b e. _om A. c e. _om ( ( G ` b ) = ( G ` c ) -> b = c ) )
27 dff13 
 |-  ( G : _om -1-1-> A <-> ( G : _om --> A /\ A. b e. _om A. c e. _om ( ( G ` b ) = ( G ` c ) -> b = c ) ) )
28 5 26 27 sylanbrc 
 |-  ( ph -> G : _om -1-1-> A )
29 f1domg 
 |-  ( A e. V -> ( G : _om -1-1-> A -> _om ~<_ A ) )
30 28 29 syl5com 
 |-  ( ph -> ( A e. V -> _om ~<_ A ) )