constr01

Description: 0 and 1 are in all steps of the construction of constructible points. (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	constr01	$⊢ φ \to \{0, 1\} \subseteq C (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		fveq2	$⊢ m = \emptyset \to C (m) = C (\emptyset)$
4	3	sseq2d	$⊢ m = \emptyset \to (\{0, 1\} \subseteq C (m) \leftrightarrow \{0, 1\} \subseteq C (\emptyset))$
5		fveq2	$⊢ m = n \to C (m) = C (n)$
6	5	sseq2d	$⊢ m = n \to (\{0, 1\} \subseteq C (m) \leftrightarrow \{0, 1\} \subseteq C (n))$
7		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
8	7	sseq2d	$⊢ m = suc n \to (\{0, 1\} \subseteq C (m) \leftrightarrow \{0, 1\} \subseteq C (suc n))$
9		fveq2	$⊢ m = N \to C (m) = C (N)$
10	9	sseq2d	$⊢ m = N \to (\{0, 1\} \subseteq C (m) \leftrightarrow \{0, 1\} \subseteq C (N))$
11	1	constr0	$⊢ C (\emptyset) = \{0, 1\}$
12	11	eqimss2i	$⊢ \{0, 1\} \subseteq C (\emptyset)$
13		simpr	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to \{0, 1\} \subseteq C (n)$
14		simpl	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to n \in On$
15		0elpr01	$⊢ 0 \in \{0, 1\}$
16	15	a1i	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to 0 \in \{0, 1\}$
17	13 16	sseldd	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to 0 \in C (n)$
18	1 14 17	constrsslem	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to C (n) \subseteq C (suc n)$
19	13 18	sstrd	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to \{0, 1\} \subseteq C (suc n)$
20	19	ex	$⊢ n \in On \to (\{0, 1\} \subseteq C (n) \to \{0, 1\} \subseteq C (suc n))$
21		0ellim	$⊢ Lim m \to \emptyset \in m$
22		fveq2	$⊢ o = \emptyset \to C (o) = C (\emptyset)$
23	22 11	eqtrdi	$⊢ o = \emptyset \to C (o) = \{0, 1\}$
24	23	ssiun2s	$⊢ \emptyset \in m \to \{0, 1\} \subseteq ⋃_{o \in m} C (o)$
25	21 24	syl	$⊢ Lim m \to \{0, 1\} \subseteq ⋃_{o \in m} C (o)$
26		vex	$⊢ m \in V$
27	26	a1i	$⊢ Lim m \to m \in V$
28		id	$⊢ Lim m \to Lim m$
29	1 27 28	constrlim	$⊢ Lim m \to C (m) = ⋃_{o \in m} C (o)$
30	25 29	sseqtrrd	$⊢ Lim m \to \{0, 1\} \subseteq C (m)$
31	30	a1d	$⊢ Lim m \to (\forall n \in m \{0, 1\} \subseteq C (n) \to \{0, 1\} \subseteq C (m))$
32	4 6 8 10 12 20 31	tfinds	$⊢ N \in On \to \{0, 1\} \subseteq C (N)$
33	2 32	syl	$⊢ φ \to \{0, 1\} \subseteq C (N)$

Metamath Proof Explorer

Theorem constr01

Proof