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 sseldi
 |-  ( ( ( 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 ) } )