constrfiss

Description: For any finite set A of constructible numbers, there is a n -th step ( Cn ) containing all numbers in A . (Contributed by Thierry Arnoux, 2-Nov-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\})$
	constrfiss.1	$⊢ φ \to A \subseteq Constr$
	constrfiss.2	$⊢ φ \to A \in Fin$
Assertion	constrfiss	$⊢ φ \to \exists n \in ω A \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		constrfiss.1	$⊢ φ \to A \subseteq Constr$
3		constrfiss.2	$⊢ φ \to A \in Fin$
4		sseq1	$⊢ b = \emptyset \to (b \subseteq C (n) \leftrightarrow \emptyset \subseteq C (n))$
5	4	rexbidv	$⊢ b = \emptyset \to (\exists n \in ω b \subseteq C (n) \leftrightarrow \exists n \in ω \emptyset \subseteq C (n))$
6		sseq1	$⊢ b = i \to (b \subseteq C (n) \leftrightarrow i \subseteq C (n))$
7	6	rexbidv	$⊢ b = i \to (\exists n \in ω b \subseteq C (n) \leftrightarrow \exists n \in ω i \subseteq C (n))$
8		sseq1	$⊢ b = i \cup \{x\} \to (b \subseteq C (n) \leftrightarrow i \cup \{x\} \subseteq C (n))$
9	8	rexbidv	$⊢ b = i \cup \{x\} \to (\exists n \in ω b \subseteq C (n) \leftrightarrow \exists n \in ω i \cup \{x\} \subseteq C (n))$
10		fveq2	$⊢ n = m \to C (n) = C (m)$
11	10	sseq2d	$⊢ n = m \to (i \cup \{x\} \subseteq C (n) \leftrightarrow i \cup \{x\} \subseteq C (m))$
12	11	cbvrexvw	$⊢ \exists n \in ω i \cup \{x\} \subseteq C (n) \leftrightarrow \exists m \in ω i \cup \{x\} \subseteq C (m)$
13	9 12	bitrdi	$⊢ b = i \cup \{x\} \to (\exists n \in ω b \subseteq C (n) \leftrightarrow \exists m \in ω i \cup \{x\} \subseteq C (m))$
14		sseq1	$⊢ b = A \to (b \subseteq C (n) \leftrightarrow A \subseteq C (n))$
15	14	rexbidv	$⊢ b = A \to (\exists n \in ω b \subseteq C (n) \leftrightarrow \exists n \in ω A \subseteq C (n))$
16		peano1	$⊢ \emptyset \in ω$
17	16	ne0ii	$⊢ ω \neq \emptyset$
18		0ss	$⊢ \emptyset \subseteq C (n)$
19	18	a1i	$⊢ (φ \land n \in ω) \to \emptyset \subseteq C (n)$
20	19	reximdva0	$⊢ (φ \land ω \neq \emptyset) \to \exists n \in ω \emptyset \subseteq C (n)$
21	17 20	mpan2	$⊢ φ \to \exists n \in ω \emptyset \subseteq C (n)$
22		simpllr	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to l \in ω$
23		fveq2	$⊢ m = l \to C (m) = C (l)$
24	23	sseq2d	$⊢ m = l \to (i \cup \{x\} \subseteq C (m) \leftrightarrow i \cup \{x\} \subseteq C (l))$
25	24	adantl	$⊢ ((((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \land m = l) \to (i \cup \{x\} \subseteq C (m) \leftrightarrow i \cup \{x\} \subseteq C (l))$
26		simp-4r	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to i \subseteq C (n)$
27		nnon	$⊢ l \in ω \to l \in On$
28	27	adantr	$⊢ (l \in ω \land n \in l) \to l \in On$
29		simpr	$⊢ (l \in ω \land n \in l) \to n \in l$
30	1 28 29	constrmon	$⊢ (l \in ω \land n \in l) \to C (n) \subseteq C (l)$
31	22 30	sylancom	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to C (n) \subseteq C (l)$
32	26 31	sstrd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to i \subseteq C (l)$
33		simplr	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to x \in C (l)$
34	33	snssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to \{x\} \subseteq C (l)$
35	32 34	unssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to i \cup \{x\} \subseteq C (l)$
36	22 25 35	rspcedvd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n \in l) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
37		simp-5r	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to n \in ω$
38		fveq2	$⊢ m = n \to C (m) = C (n)$
39	38	sseq2d	$⊢ m = n \to (i \cup \{x\} \subseteq C (m) \leftrightarrow i \cup \{x\} \subseteq C (n))$
40	39	adantl	$⊢ ((((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \land m = n) \to (i \cup \{x\} \subseteq C (m) \leftrightarrow i \cup \{x\} \subseteq C (n))$
41		simp-4r	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to i \subseteq C (n)$
42		nnon	$⊢ n \in ω \to n \in On$
43	42	adantr	$⊢ (n \in ω \land l \in n) \to n \in On$
44		simpr	$⊢ (n \in ω \land l \in n) \to l \in n$
45	1 43 44	constrmon	$⊢ (n \in ω \land l \in n) \to C (l) \subseteq C (n)$
46	37 45	sylancom	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to C (l) \subseteq C (n)$
47		simplr	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to x \in C (l)$
48	46 47	sseldd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to x \in C (n)$
49	48	snssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to \{x\} \subseteq C (n)$
50	41 49	unssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to i \cup \{x\} \subseteq C (n)$
51	37 40 50	rspcedvd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land l \in n) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
52		simp-5r	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to n \in ω$
53	39	adantl	$⊢ ((((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \land m = n) \to (i \cup \{x\} \subseteq C (m) \leftrightarrow i \cup \{x\} \subseteq C (n))$
54		simp-4r	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to i \subseteq C (n)$
55		simplr	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to x \in C (l)$
56		simpr	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to n = l$
57	56	fveq2d	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to C (n) = C (l)$
58	55 57	eleqtrrd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to x \in C (n)$
59	58	snssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to \{x\} \subseteq C (n)$
60	54 59	unssd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to i \cup \{x\} \subseteq C (n)$
61	52 53 60	rspcedvd	$⊢ (((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \land n = l) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
62	42	ad4antlr	$⊢ ((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \to n \in On$
63	27	ad2antlr	$⊢ ((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \to l \in On$
64		oneltri	$⊢ (n \in On \land l \in On) \to (n \in l \lor l \in n \lor n = l)$
65	62 63 64	syl2anc	$⊢ ((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \to (n \in l \lor l \in n \lor n = l)$
66	36 51 61 65	mpjao3dan	$⊢ ((((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \land l \in ω) \land x \in C (l)) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
67	2	ad4antr	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to A \subseteq Constr$
68		simpllr	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to x \in (A ∖ i)$
69	68	eldifad	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to x \in A$
70	67 69	sseldd	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to x \in Constr$
71	1	isconstr	$⊢ x \in Constr \leftrightarrow \exists l \in ω x \in C (l)$
72	70 71	sylib	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to \exists l \in ω x \in C (l)$
73	66 72	r19.29a	$⊢ ((((φ \land i \subseteq A) \land x \in (A ∖ i)) \land n \in ω) \land i \subseteq C (n)) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
74	73	r19.29an	$⊢ (((φ \land i \subseteq A) \land x \in (A ∖ i)) \land \exists n \in ω i \subseteq C (n)) \to \exists m \in ω i \cup \{x\} \subseteq C (m)$
75	74	ex	$⊢ ((φ \land i \subseteq A) \land x \in (A ∖ i)) \to (\exists n \in ω i \subseteq C (n) \to \exists m \in ω i \cup \{x\} \subseteq C (m))$
76	75	anasss	$⊢ (φ \land (i \subseteq A \land x \in (A ∖ i))) \to (\exists n \in ω i \subseteq C (n) \to \exists m \in ω i \cup \{x\} \subseteq C (m))$
77	5 7 13 15 21 76 3	findcard2d	$⊢ φ \to \exists n \in ω A \subseteq C (n)$

Metamath Proof Explorer

Theorem constrfiss

Proof