Theorem constrss

Description: Constructed points are in the next generation constructed points. (Contributed by Thierry Arnoux, 25-Jun-2025)

	Ref	Expression
Hypotheses	constr0.1	|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
	constrsscn.1	|- ( ph -> N e. On )
Assertion	constrss	|- ( ph -> ( C ` N ) C_ ( C ` suc N ) )

Proof

Step	Hyp	Ref	Expression
1		constr0.1	|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
2		constrsscn.1	|- ( ph -> N e. On )
3	1 2	constr01	|- ( ph -> { 0 , 1 } C_ ( C ` N ) )
4		c0ex	|- 0 e. _V
5	4	prid1	|- 0 e. { 0 , 1 }
6	5	a1i	|- ( ph -> 0 e. { 0 , 1 } )
7	3 6	sseldd	|- ( ph -> 0 e. ( C ` N ) )
8	1 2 7	constrsslem	|- ( ph -> ( C ` N ) C_ ( C ` suc N ) )