Theorem erdszelem3

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 , < ) )
Assertion	erdszelem3	|- ( A e. ( 1 ... N ) -> ( K ` A ) = sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) )

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		oveq2	|- ( x = A -> ( 1 ... x ) = ( 1 ... A ) )
5	4	pweqd	|- ( x = A -> ~P ( 1 ... x ) = ~P ( 1 ... A ) )
6		eleq1	|- ( x = A -> ( x e. y <-> A e. y ) )
7	6	anbi2d	|- ( x = A -> ( ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) <-> ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) ) )
8	5 7	rabeqbidv	|- ( x = A -> { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } )
9	8	imaeq2d	|- ( x = A -> ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) = ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
10	9	supeq1d	|- ( x = A -> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) = sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) )
11		ltso	|- < Or RR
12	11	supex	|- sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) e. _V
13	10 3 12	fvmpt	|- ( A e. ( 1 ... N ) -> ( K ` A ) = sup ( ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) , RR , < ) )