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		c0ex	$⊢ 0 \in V$
16	15	prid1	$⊢ 0 \in \{0, 1\}$
17	16	a1i	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to 0 \in \{0, 1\}$
18	13 17	sseldd	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to 0 \in C (n)$
19	1 14 18	constrsslem	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to C (n) \subseteq C (suc n)$
20	13 19	sstrd	$⊢ (n \in On \land \{0, 1\} \subseteq C (n)) \to \{0, 1\} \subseteq C (suc n)$
21	20	ex	$⊢ n \in On \to (\{0, 1\} \subseteq C (n) \to \{0, 1\} \subseteq C (suc n))$
22		0ellim	$⊢ Lim m \to \emptyset \in m$
23		fveq2	$⊢ o = \emptyset \to C (o) = C (\emptyset)$
24	23 11	eqtrdi	$⊢ o = \emptyset \to C (o) = \{0, 1\}$
25	24	ssiun2s	$⊢ \emptyset \in m \to \{0, 1\} \subseteq ⋃_{o \in m} C (o)$
26	22 25	syl	$⊢ Lim m \to \{0, 1\} \subseteq ⋃_{o \in m} C (o)$
27		vex	$⊢ m \in V$
28	27	a1i	$⊢ Lim m \to m \in V$
29		id	$⊢ Lim m \to Lim m$
30	1 28 29	constrlim	$⊢ Lim m \to C (m) = ⋃_{o \in m} C (o)$
31	26 30	sseqtrrd	$⊢ Lim m \to \{0, 1\} \subseteq C (m)$
32	31	a1d	$⊢ Lim m \to (\forall n \in m \{0, 1\} \subseteq C (n) \to \{0, 1\} \subseteq C (m))$
33	4 6 8 10 12 21 32	tfinds	$⊢ N \in On \to \{0, 1\} \subseteq C (N)$
34	2 33	syl	$⊢ φ \to \{0, 1\} \subseteq C (N)$

Metamath Proof Explorer

Theorem constr01

Proof