Metamath Proof Explorer

Theorem erdszelem7

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.k 
|- K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.o 
|- O Or RR
erdszelem.a 
|- ( ph -> A e. ( 1 ... N ) )
erdszelem7.r 
|- ( ph -> R e. NN )
erdszelem7.m 
|- ( ph -> -. ( K ` A ) e. ( 1 ... ( R - 1 ) ) )
Assertion erdszelem7 
|- ( ph -> E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( 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.k 
 |-  K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
4 erdszelem.o 
 |-  O Or RR
5 erdszelem.a 
 |-  ( ph -> A e. ( 1 ... N ) )
6 erdszelem7.r 
 |-  ( ph -> R e. NN )
7 erdszelem7.m 
 |-  ( ph -> -. ( K ` A ) e. ( 1 ... ( R - 1 ) ) )
8 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
9 ffun 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> Fun # )
10 8 9 ax-mp 
 |-  Fun #
11 1 2 3 4 erdszelem5 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
12 5 11 mpdan 
 |-  ( ph -> ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
13 fvelima 
 |-  ( ( Fun # /\ ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) ) -> E. s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` s ) = ( K ` A ) )
14 10 12 13 sylancr 
 |-  ( ph -> E. s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` s ) = ( K ` A ) )
15 eqid 
 |-  { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
16 15 erdszelem1 
 |-  ( s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } <-> ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) )
17 simprl1 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> s C_ ( 1 ... A ) )
18 elfzuz3 
 |-  ( A e. ( 1 ... N ) -> N e. ( ZZ>= ` A ) )
19 fzss2 
 |-  ( N e. ( ZZ>= ` A ) -> ( 1 ... A ) C_ ( 1 ... N ) )
20 5 18 19 3syl 
 |-  ( ph -> ( 1 ... A ) C_ ( 1 ... N ) )
21 20 adantr 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> ( 1 ... A ) C_ ( 1 ... N ) )
22 17 21 sstrd 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> s C_ ( 1 ... N ) )
23 velpw 
 |-  ( s e. ~P ( 1 ... N ) <-> s C_ ( 1 ... N ) )
24 22 23 sylibr 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> s e. ~P ( 1 ... N ) )
25 1 2 3 4 erdszelem6 
 |-  ( ph -> K : ( 1 ... N ) --> NN )
26 25 5 ffvelrnd 
 |-  ( ph -> ( K ` A ) e. NN )
27 nnuz 
 |-  NN = ( ZZ>= ` 1 )
28 26 27 eleqtrdi 
 |-  ( ph -> ( K ` A ) e. ( ZZ>= ` 1 ) )
29 nnz 
 |-  ( R e. NN -> R e. ZZ )
30 peano2zm 
 |-  ( R e. ZZ -> ( R - 1 ) e. ZZ )
31 6 29 30 3syl 
 |-  ( ph -> ( R - 1 ) e. ZZ )
32 elfz5 
 |-  ( ( ( K ` A ) e. ( ZZ>= ` 1 ) /\ ( R - 1 ) e. ZZ ) -> ( ( K ` A ) e. ( 1 ... ( R - 1 ) ) <-> ( K ` A ) <_ ( R - 1 ) ) )
33 28 31 32 syl2anc 
 |-  ( ph -> ( ( K ` A ) e. ( 1 ... ( R - 1 ) ) <-> ( K ` A ) <_ ( R - 1 ) ) )
34 nnltlem1 
 |-  ( ( ( K ` A ) e. NN /\ R e. NN ) -> ( ( K ` A ) < R <-> ( K ` A ) <_ ( R - 1 ) ) )
35 26 6 34 syl2anc 
 |-  ( ph -> ( ( K ` A ) < R <-> ( K ` A ) <_ ( R - 1 ) ) )
36 33 35 bitr4d 
 |-  ( ph -> ( ( K ` A ) e. ( 1 ... ( R - 1 ) ) <-> ( K ` A ) < R ) )
37 7 36 mtbid 
 |-  ( ph -> -. ( K ` A ) < R )
38 6 nnred 
 |-  ( ph -> R e. RR )
39 15 erdszelem2 
 |-  ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) e. Fin /\ ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ NN )
40 39 simpri 
 |-  ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ NN
41 nnssre 
 |-  NN C_ RR
42 40 41 sstri 
 |-  ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ RR
43 42 12 sselid 
 |-  ( ph -> ( K ` A ) e. RR )
44 38 43 lenltd 
 |-  ( ph -> ( R <_ ( K ` A ) <-> -. ( K ` A ) < R ) )
45 37 44 mpbird 
 |-  ( ph -> R <_ ( K ` A ) )
46 45 adantr 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> R <_ ( K ` A ) )
47 simprr 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> ( # ` s ) = ( K ` A ) )
48 46 47 breqtrrd 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> R <_ ( # ` s ) )
49 simprl2 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> ( F |` s ) Isom < , O ( s , ( F " s ) ) )
50 24 48 49 jca32 
 |-  ( ( ph /\ ( ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) /\ ( # ` s ) = ( K ` A ) ) ) -> ( s e. ~P ( 1 ... N ) /\ ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) ) )
51 50 expr 
 |-  ( ( ph /\ ( s C_ ( 1 ... A ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) /\ A e. s ) ) -> ( ( # ` s ) = ( K ` A ) -> ( s e. ~P ( 1 ... N ) /\ ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) ) ) )
52 16 51 sylan2b 
 |-  ( ( ph /\ s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) -> ( ( # ` s ) = ( K ` A ) -> ( s e. ~P ( 1 ... N ) /\ ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) ) ) )
53 52 expimpd 
 |-  ( ph -> ( ( s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } /\ ( # ` s ) = ( K ` A ) ) -> ( s e. ~P ( 1 ... N ) /\ ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) ) ) )
54 53 reximdv2 
 |-  ( ph -> ( E. s e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` s ) = ( K ` A ) -> E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) ) )
55 14 54 mpd 
 |-  ( ph -> E. s e. ~P ( 1 ... N ) ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , O ( s , ( F " s ) ) ) )