constrmon

Description: The construction of constructible numbers is monotonous, i.e. if the ordinal M is less than the ordinal N , which is denoted by M e. N , then the M -th step of the constructible numbers is included in the N -th step. (Contributed by Thierry Arnoux, 1-Jul-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$
	constrmon.1	$⊢ φ \to M \in N$
Assertion	constrmon	$⊢ φ \to C (M) \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		constrmon.1	$⊢ φ \to M \in N$
4		eleq2	$⊢ m = \emptyset \to (M \in m \leftrightarrow M \in \emptyset)$
5		fveq2	$⊢ m = \emptyset \to C (m) = C (\emptyset)$
6	5	sseq2d	$⊢ m = \emptyset \to (C (M) \subseteq C (m) \leftrightarrow C (M) \subseteq C (\emptyset))$
7	4 6	imbi12d	$⊢ m = \emptyset \to ((M \in m \to C (M) \subseteq C (m)) \leftrightarrow (M \in \emptyset \to C (M) \subseteq C (\emptyset)))$
8		eleq2w	$⊢ m = n \to (M \in m \leftrightarrow M \in n)$
9		fveq2	$⊢ m = n \to C (m) = C (n)$
10	9	sseq2d	$⊢ m = n \to (C (M) \subseteq C (m) \leftrightarrow C (M) \subseteq C (n))$
11	8 10	imbi12d	$⊢ m = n \to ((M \in m \to C (M) \subseteq C (m)) \leftrightarrow (M \in n \to C (M) \subseteq C (n)))$
12		eleq2	$⊢ m = suc n \to (M \in m \leftrightarrow M \in suc n)$
13		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
14	13	sseq2d	$⊢ m = suc n \to (C (M) \subseteq C (m) \leftrightarrow C (M) \subseteq C (suc n))$
15	12 14	imbi12d	$⊢ m = suc n \to ((M \in m \to C (M) \subseteq C (m)) \leftrightarrow (M \in suc n \to C (M) \subseteq C (suc n)))$
16		eleq2	$⊢ m = N \to (M \in m \leftrightarrow M \in N)$
17		fveq2	$⊢ m = N \to C (m) = C (N)$
18	17	sseq2d	$⊢ m = N \to (C (M) \subseteq C (m) \leftrightarrow C (M) \subseteq C (N))$
19	16 18	imbi12d	$⊢ m = N \to ((M \in m \to C (M) \subseteq C (m)) \leftrightarrow (M \in N \to C (M) \subseteq C (N)))$
20		noel	$⊢ \neg M \in \emptyset$
21	20	pm2.21i	$⊢ M \in \emptyset \to C (M) \subseteq C (\emptyset)$
22		simpllr	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M \in n) \to (M \in n \to C (M) \subseteq C (n))$
23	22	syldbl2	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M \in n) \to C (M) \subseteq C (n)$
24		simplll	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M \in n) \to n \in On$
25	1 24	constrss	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M \in n) \to C (n) \subseteq C (suc n)$
26	23 25	sstrd	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M \in n) \to C (M) \subseteq C (suc n)$
27		simpr	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M = n) \to M = n$
28	27	fveq2d	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M = n) \to C (M) = C (n)$
29		simplll	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M = n) \to n \in On$
30	1 29	constrss	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M = n) \to C (n) \subseteq C (suc n)$
31	28 30	eqsstrd	$⊢ (((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \land M = n) \to C (M) \subseteq C (suc n)$
32		simpr	$⊢ ((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \to M \in suc n$
33		elsuci	$⊢ M \in suc n \to (M \in n \lor M = n)$
34	32 33	syl	$⊢ ((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \to (M \in n \lor M = n)$
35	26 31 34	mpjaodan	$⊢ ((n \in On \land (M \in n \to C (M) \subseteq C (n))) \land M \in suc n) \to C (M) \subseteq C (suc n)$
36	35	exp31	$⊢ n \in On \to ((M \in n \to C (M) \subseteq C (n)) \to (M \in suc n \to C (M) \subseteq C (suc n)))$
37		fveq2	$⊢ i = M \to C (i) = C (M)$
38	37	sseq2d	$⊢ i = M \to (C (M) \subseteq C (i) \leftrightarrow C (M) \subseteq C (M))$
39		simpr	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to M \in m$
40		ssidd	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to C (M) \subseteq C (M)$
41	38 39 40	rspcedvdw	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to \exists i \in m C (M) \subseteq C (i)$
42		ssiun	$⊢ \exists i \in m C (M) \subseteq C (i) \to C (M) \subseteq ⋃_{i \in m} C (i)$
43	41 42	syl	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to C (M) \subseteq ⋃_{i \in m} C (i)$
44		vex	$⊢ m \in V$
45	44	a1i	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to m \in V$
46		simpll	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to Lim m$
47	1 45 46	constrlim	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to C (m) = ⋃_{i \in m} C (i)$
48	43 47	sseqtrrd	$⊢ ((Lim m \land \forall n \in m (M \in n \to C (M) \subseteq C (n))) \land M \in m) \to C (M) \subseteq C (m)$
49	48	exp31	$⊢ Lim m \to (\forall n \in m (M \in n \to C (M) \subseteq C (n)) \to (M \in m \to C (M) \subseteq C (m)))$
50	7 11 15 19 21 36 49	tfinds	$⊢ N \in On \to (M \in N \to C (M) \subseteq C (N))$
51	2 3 50	sylc	$⊢ φ \to C (M) \subseteq C (N)$

Metamath Proof Explorer

Theorem constrmon

Proof