Metamath Proof Explorer


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 V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
constrsscn.1 φ N On
Assertion constrss φ C N C suc N

Proof

Step Hyp Ref Expression
1 constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
2 constrsscn.1 φ N On
3 1 2 constr01 φ 0 1 C N
4 c0ex 0 V
5 4 prid1 0 0 1
6 5 a1i φ 0 0 1
7 3 6 sseldd φ 0 C N
8 1 2 7 constrsslem φ C N C suc N