Metamath Proof Explorer

Theorem erdszelem5

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 erdszelem5 
|- ( ( ph /\ A e. ( 1 ... N ) ) -> ( K ` 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 1 2 3 erdszelem3 
 |-  ( A e. ( 1 ... N ) -> ( K ` A ) = sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) )
6 5 adantl 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( K ` A ) = sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) )
7 snex 
 |-  { A } e. _V
8 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
9 8 fdmi 
 |-  dom # = _V
10 7 9 eleqtrri 
 |-  { A } e. dom #
11 1 2 3 4 erdszelem4 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } )
12 inelcm 
 |-  ( ( { A } e. dom # /\ { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) -> ( dom # i^i { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) )
13 10 11 12 sylancr 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( dom # i^i { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) )
14 imadisj 
 |-  ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) = (/) <-> ( dom # i^i { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) = (/) )
15 14 necon3bii 
 |-  ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) <-> ( dom # i^i { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) )
16 13 15 sylibr 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) )
17 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 ) }
18 17 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 )
19 18 simpli 
 |-  ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) e. Fin
20 18 simpri 
 |-  ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ NN
21 nnssre 
 |-  NN C_ RR
22 20 21 sstri 
 |-  ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ RR
23 ltso 
 |-  < Or RR
24 fisupcl 
 |-  ( ( < Or RR /\ ( ( # " { 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 ) } ) =/= (/) /\ ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ RR ) ) -> sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
25 23 24 mpan 
 |-  ( ( ( # " { 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 ) } ) =/= (/) /\ ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) C_ RR ) -> sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
26 19 22 25 mp3an13 
 |-  ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) =/= (/) -> sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
27 16 26 syl 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
28 6 27 eqeltrd 
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )