Metamath Proof Explorer

Theorem erdszelem4

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
Assertion erdszelem4 
|- ( ( ph /\ A e. ( 1 ... N ) ) -> { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } )

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 elfznn 
 |-  ( A e. ( 1 ... N ) -> A e. NN )
6 5 adantl 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> A e. NN )
7 elfz1end 
 |-  ( A e. NN <-> A e. ( 1 ... A ) )
8 6 7 sylib 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> A e. ( 1 ... A ) )
9 8 snssd 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> { A } C_ ( 1 ... A ) )
10 elsni 
 |-  ( x e. { A } -> x = A )
11 elsni 
 |-  ( y e. { A } -> y = A )
12 10 11 breqan12d 
 |-  ( ( x e. { A } /\ y e. { A } ) -> ( x < y <-> A < A ) )
13 12 adantl 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( x < y <-> A < A ) )
14 fzssuz 
 |-  ( 1 ... N ) C_ ( ZZ>= ` 1 )
15 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
16 zssre 
 |-  ZZ C_ RR
17 15 16 sstri 
 |-  ( ZZ>= ` 1 ) C_ RR
18 14 17 sstri 
 |-  ( 1 ... N ) C_ RR
19 simpr 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> A e. ( 1 ... N ) )
20 19 adantr 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> A e. ( 1 ... N ) )
21 18 20 sselid 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> A e. RR )
22 21 ltnrd 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> -. A < A )
23 22 pm2.21d 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( A < A -> ( F ` x ) O ( F ` y ) ) )
24 13 23 sylbid 
 |-  ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( x < y -> ( F ` x ) O ( F ` y ) ) )
25 24 ralrimivva 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) )
26 f1f 
 |-  ( F : ( 1 ... N ) -1-1-> RR -> F : ( 1 ... N ) --> RR )
27 2 26 syl 
 |-  ( ph -> F : ( 1 ... N ) --> RR )
28 27 adantr 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> F : ( 1 ... N ) --> RR )
29 19 snssd 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> { A } C_ ( 1 ... N ) )
30 ltso 
 |-  < Or RR
31 soss 
 |-  ( ( 1 ... N ) C_ RR -> ( < Or RR -> < Or ( 1 ... N ) ) )
32 18 30 31 mp2 
 |-  < Or ( 1 ... N )
33 soisores 
 |-  ( ( ( < Or ( 1 ... N ) /\ O Or RR ) /\ ( F : ( 1 ... N ) --> RR /\ { A } C_ ( 1 ... N ) ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) )
34 32 4 33 mpanl12 
 |-  ( ( F : ( 1 ... N ) --> RR /\ { A } C_ ( 1 ... N ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) )
35 28 29 34 syl2anc 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) )
36 25 35 mpbird 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) )
37 snidg 
 |-  ( A e. ( 1 ... N ) -> A e. { A } )
38 37 adantl 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> A e. { A } )
39 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 ) }
40 39 erdszelem1 
 |-  ( { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } <-> ( { A } C_ ( 1 ... A ) /\ ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) /\ A e. { A } ) )
41 9 36 38 40 syl3anbrc 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } )