Metamath Proof Explorer

Theorem constrss

Description: Constructed points are in the next generation constructed points. Lemma 7.3 of Stewart p. 91. (Contributed by Thierry Arnoux, 25-Jun-2025)

		Ref	Expression
	Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
		constrsscn.1	$⊢ φ \to N \in On$
	Assertion	constrss	$⊢ φ \to C (N) \subseteq C (suc N)$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrsscn.1	$⊢ φ \to N \in On$
3	1 2	constr01	$⊢ φ \to \{0, 1\} \subseteq C (N)$
4		0elpr01	$⊢ 0 \in \{0, 1\}$
5	4	a1i	$⊢ φ \to 0 \in \{0, 1\}$
6	3 5	sseldd	$⊢ φ \to 0 \in C (N)$
7	1 2 6	constrsslem	$⊢ φ \to C (N) \subseteq C (suc N)$