Metamath Proof Explorer

Theorem erdszelem11

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n 
|- ( ph -> N e. NN )
erdsze.f 
|- ( ph -> F : ( 1 ... N ) -1-1-> RR )
erdszelem.i 
|- I = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.j 
|- J = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.t 
|- T = ( n e. ( 1 ... N ) |-> <. ( I ` n ) , ( J ` n ) >. )
erdszelem.r 
|- ( ph -> R e. NN )
erdszelem.s 
|- ( ph -> S e. NN )
erdszelem.m 
|- ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
Assertion erdszelem11 
|- ( ph -> E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n 
 |-  ( ph -> N e. NN )
2 erdsze.f 
 |-  ( ph -> F : ( 1 ... N ) -1-1-> RR )
3 erdszelem.i 
 |-  I = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
4 erdszelem.j 
 |-  J = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
5 erdszelem.t 
 |-  T = ( n e. ( 1 ... N ) |-> <. ( I ` n ) , ( J ` n ) >. )
6 erdszelem.r 
 |-  ( ph -> R e. NN )
7 erdszelem.s 
 |-  ( ph -> S e. NN )
8 erdszelem.m 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
9 1 2 3 4 5 6 7 8 erdszelem10 
 |-  ( ph -> E. m e. ( 1 ... N ) ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) )
10 1 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> N e. NN )
11 2 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> F : ( 1 ... N ) -1-1-> RR )
12 ltso 
 |-  < Or RR
13 simprl 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> m e. ( 1 ... N ) )
14 6 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> R e. NN )
15 simprr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) )
16 10 11 3 12 13 14 15 erdszelem7 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) ) ) -> E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) )
17 16 expr 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) -> E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) ) )
18 1 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> N e. NN )
19 2 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> F : ( 1 ... N ) -1-1-> RR )
20 gtso 
 |-  `' < Or RR
21 simprl 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> m e. ( 1 ... N ) )
22 7 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> S e. NN )
23 simprr 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) )
24 18 19 4 20 21 22 23 erdszelem7 
 |-  ( ( ph /\ ( m e. ( 1 ... N ) /\ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) -> E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) )
25 24 expr 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) -> E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )
26 17 25 orim12d 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) -> ( E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) )
27 26 rexlimdva 
 |-  ( ph -> ( E. m e. ( 1 ... N ) ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) -> ( E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) )
28 9 27 mpd 
 |-  ( ph -> ( E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )
29 r19.43 
 |-  ( E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) <-> ( E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ E. s e. ~P ( 1 ... N ) ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )
30 28 29 sylibr 
 |-  ( ph -> E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )