Metamath Proof Explorer

Theorem erdszelem6

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 erdszelem6 
|- ( ph -> K : ( 1 ... N ) --> NN )

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 ltso 
 |-  < Or RR
6 5 supex 
 |-  sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) e. _V
7 6 a1i 
 |-  ( ( ph /\ x e. ( 1 ... N ) ) -> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) e. _V )
8 3 a1i 
 |-  ( ph -> K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) )
9 eqid 
 |-  { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) } = { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) }
10 9 erdszelem2 
 |-  ( ( # " { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) } ) e. Fin /\ ( # " { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) } ) C_ NN )
11 10 simpri 
 |-  ( # " { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) } ) C_ NN
12 1 2 3 4 erdszelem5 
 |-  ( ( ph /\ z e. ( 1 ... N ) ) -> ( K ` z ) e. ( # " { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ z e. y ) } ) )
13 11 12 sselid 
 |-  ( ( ph /\ z e. ( 1 ... N ) ) -> ( K ` z ) e. NN )
14 7 8 13 fmpt2d 
 |-  ( ph -> K : ( 1 ... N ) --> NN )