numtowerdt

Description: Certain number sets and fields form a tower. In particular, singleton 1, natural numbers, natural numbers with zero, integers, rationals, algebraic reals (notice that current definition allows algebraic numbers to be complex thus the restriction), reals and complex number sets are a tower of proper subsets. (Contributed by Ender Ting, 31-Jul-2026)

		Ref	Expression
	Assertion	numtowerdt	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ℂ ”⟩ \in {Chain}_{V} [\subset]$

Proof

Step	Hyp	Ref	Expression
1		df-s8	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ℂ ”⟩ = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ ++ ⟨“ ℂ ”⟩$
2		cnex	$⊢ ℂ \in V$
3	2	a1i	$⊢ ⊤ \to ℂ \in V$
4		df-s7	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ ++ ⟨“ ℝ ”⟩$
5		reex	$⊢ ℝ \in V$
6	5	a1i	$⊢ ⊤ \to ℝ \in V$
7		df-s6	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ ++ ⟨“ (𝔸 \cap ℝ) ”⟩$
8	5	inex2	$⊢ 𝔸 \cap ℝ \in V$
9	8	a1i	$⊢ ⊤ \to 𝔸 \cap ℝ \in V$
10		df-s5	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ = ⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ ++ ⟨“ ℚ ”⟩$
11		qex	$⊢ ℚ \in V$
12	11	a1i	$⊢ ⊤ \to ℚ \in V$
13		df-s4	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ = ⟨“ \{1\} ℕ ℕ_{0} ”⟩ ++ ⟨“ ℤ ”⟩$
14		zex	$⊢ ℤ \in V$
15	14	a1i	$⊢ ⊤ \to ℤ \in V$
16		df-s3	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ”⟩ = ⟨“ \{1\} ℕ ”⟩ ++ ⟨“ ℕ_{0} ”⟩$
17		nn0ex	$⊢ ℕ_{0} \in V$
18	17	a1i	$⊢ ⊤ \to ℕ_{0} \in V$
19		df-s2	$⊢ ⟨“ \{1\} ℕ ”⟩ = ⟨“ \{1\} ”⟩ ++ ⟨“ ℕ ”⟩$
20		nnex	$⊢ ℕ \in V$
21	20	a1i	$⊢ ⊤ \to ℕ \in V$
22		snex	$⊢ \{1\} \in V$
23	22	a1i	$⊢ ⊤ \to \{1\} \in V$
24	23	s1chn	$⊢ ⊤ \to ⟨“ \{1\} ”⟩ \in {Chain}_{V} [\subset]$
25		lsws1	$⊢ \{1\} \in V \to lastS (⟨“ \{1\} ”⟩) = \{1\}$
26	22 25	ax-mp	$⊢ lastS (⟨“ \{1\} ”⟩) = \{1\}$
27		1nn	$⊢ 1 \in ℕ$
28		1ex	$⊢ 1 \in V$
29	28	snss	$⊢ 1 \in ℕ \leftrightarrow \{1\} \subseteq ℕ$
30	27 29	mpbi	$⊢ \{1\} \subseteq ℕ$
31		2nn	$⊢ 2 \in ℕ$
32		1re	$⊢ 1 \in ℝ$
33		1lt2	$⊢ 1 < 2$
34	32 33	gtneii	$⊢ 2 \neq 1$
35		nelsn	$⊢ 2 \neq 1 \to \neg 2 \in \{1\}$
36	34 35	ax-mp	$⊢ \neg 2 \in \{1\}$
37	31 36	pm3.2i	$⊢ (2 \in ℕ \land \neg 2 \in \{1\})$
38		ssnelpss	$⊢ \{1\} \subseteq ℕ \to ((2 \in ℕ \land \neg 2 \in \{1\}) \to \{1\} \subset ℕ)$
39	30 37 38	mp2	$⊢ \{1\} \subset ℕ$
40	20	brrpss	$⊢ \{1\} [\subset] ℕ \leftrightarrow \{1\} \subset ℕ$
41	39 40	mpbir	$⊢ \{1\} [\subset] ℕ$
42	26 41	eqbrtri	$⊢ lastS (⟨“ \{1\} ”⟩) [\subset] ℕ$
43	42	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ”⟩) [\subset] ℕ$
44	43	olcd	$⊢ ⊤ \to (⟨“ \{1\} ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ”⟩) [\subset] ℕ)$
45	21 24 44	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ”⟩ ++ ⟨“ ℕ ”⟩ \in {Chain}_{V} [\subset]$
46	19 45	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ”⟩ \in {Chain}_{V} [\subset]$
47		lsws2	$⊢ ℕ \in V \to lastS (⟨“ \{1\} ℕ ”⟩) = ℕ$
48	20 47	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ”⟩) = ℕ$
49		nthruz	$⊢ (ℕ \subset ℕ_{0} \land ℕ_{0} \subset ℤ)$
50	49	simpli	$⊢ ℕ \subset ℕ_{0}$
51	17	brrpss	$⊢ ℕ [\subset] ℕ_{0} \leftrightarrow ℕ \subset ℕ_{0}$
52	50 51	mpbir	$⊢ ℕ [\subset] ℕ_{0}$
53	48 52	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ”⟩) [\subset] ℕ_{0}$
54	53	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ”⟩) [\subset] ℕ_{0}$
55	54	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ”⟩) [\subset] ℕ_{0})$
56	18 46 55	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ”⟩ ++ ⟨“ ℕ_{0} ”⟩ \in {Chain}_{V} [\subset]$
57	16 56	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ”⟩ \in {Chain}_{V} [\subset]$
58		lsws3	$⊢ ℕ_{0} \in V \to lastS (⟨“ \{1\} ℕ ℕ_{0} ”⟩) = ℕ_{0}$
59	17 58	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ”⟩) = ℕ_{0}$
60	49	simpri	$⊢ ℕ_{0} \subset ℤ$
61	14	brrpss	$⊢ ℕ_{0} [\subset] ℤ \leftrightarrow ℕ_{0} \subset ℤ$
62	60 61	mpbir	$⊢ ℕ_{0} [\subset] ℤ$
63	59 62	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ”⟩) [\subset] ℤ$
64	63	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ℕ_{0} ”⟩) [\subset] ℤ$
65	64	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ℕ_{0} ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ℕ_{0} ”⟩) [\subset] ℤ)$
66	15 57 65	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ”⟩ ++ ⟨“ ℤ ”⟩ \in {Chain}_{V} [\subset]$
67	13 66	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ \in {Chain}_{V} [\subset]$
68		lsws4	$⊢ ℤ \in V \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩) = ℤ$
69	14 68	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩) = ℤ$
70		nthruc	$⊢ ((ℕ \subset ℤ \land ℤ \subset ℚ) \land (ℚ \subset ℝ \land ℝ \subset ℂ))$
71	70	simpli	$⊢ (ℕ \subset ℤ \land ℤ \subset ℚ)$
72	71	simpri	$⊢ ℤ \subset ℚ$
73	11	brrpss	$⊢ ℤ [\subset] ℚ \leftrightarrow ℤ \subset ℚ$
74	72 73	mpbir	$⊢ ℤ [\subset] ℚ$
75	69 74	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩) [\subset] ℚ$
76	75	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩) [\subset] ℚ$
77	76	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩) [\subset] ℚ)$
78	12 67 77	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ ++ ⟨“ ℚ ”⟩ \in {Chain}_{V} [\subset]$
79	10 78	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ \in {Chain}_{V} [\subset]$
80		s5cli	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ \in Word V$
81		lsw	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ \in Word V \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| - 1)$
82	80 81	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| - 1)$
83		s5len	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| = 5$
84	83	oveq1i	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| - 1 = 5 - 1$
85		5m1e4	$⊢ 5 - 1 = 4$
86	84 85	eqtri	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| - 1 = 4$
87	86	fveq2i	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩\| - 1) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (4)$
88		s4cli	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩ \in Word V$
89		s4len	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ”⟩\| = 4$
90	10 88 89	cats1fvn	$⊢ ℚ \in V \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (4) = ℚ$
91	11 90	ax-mp	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ (4) = ℚ$
92	82 87 91	3eqtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) = ℚ$
93		qssaa	$⊢ ℚ \subseteq 𝔸$
94		qssre	$⊢ ℚ \subseteq ℝ$
95	93 94	ssini	$⊢ ℚ \subseteq 𝔸 \cap ℝ$
96		sqrtnnaa	$⊢ 2 \in ℕ \to \sqrt{2} \in 𝔸$
97	31 96	ax-mp	$⊢ \sqrt{2} \in 𝔸$
98		sqrt2re	$⊢ \sqrt{2} \in ℝ$
99	97 98	elini	$⊢ \sqrt{2} \in (𝔸 \cap ℝ)$
100		sqrt2irr	$⊢ \sqrt{2} \notin ℚ$
101	100	neli	$⊢ \neg \sqrt{2} \in ℚ$
102	99 101	pm3.2i	$⊢ (\sqrt{2} \in (𝔸 \cap ℝ) \land \neg \sqrt{2} \in ℚ)$
103		ssnelpss	$⊢ ℚ \subseteq 𝔸 \cap ℝ \to ((\sqrt{2} \in (𝔸 \cap ℝ) \land \neg \sqrt{2} \in ℚ) \to ℚ \subset 𝔸 \cap ℝ)$
104	95 102 103	mp2	$⊢ ℚ \subset 𝔸 \cap ℝ$
105	8	brrpss	$⊢ ℚ [\subset] (𝔸 \cap ℝ) \leftrightarrow ℚ \subset 𝔸 \cap ℝ$
106	104 105	mpbir	$⊢ ℚ [\subset] (𝔸 \cap ℝ)$
107	92 106	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) [\subset] (𝔸 \cap ℝ)$
108	107	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) [\subset] (𝔸 \cap ℝ)$
109	108	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩) [\subset] (𝔸 \cap ℝ))$
110	9 79 109	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ ”⟩ ++ ⟨“ (𝔸 \cap ℝ) ”⟩ \in {Chain}_{V} [\subset]$
111	7 110	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ \in {Chain}_{V} [\subset]$
112		s6cli	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ \in Word V$
113		lsw	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ \in Word V \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| - 1)$
114	112 113	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| - 1)$
115		s6len	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| = 6$
116	115	oveq1i	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| - 1 = 6 - 1$
117		6m1e5	$⊢ 6 - 1 = 5$
118	116 117	eqtri	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| - 1 = 5$
119	118	fveq2i	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩\| - 1) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (5)$
120	7 80 83	cats1fvn	$⊢ 𝔸 \cap ℝ \in V \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (5) = 𝔸 \cap ℝ$
121	8 120	ax-mp	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ (5) = 𝔸 \cap ℝ$
122	114 119 121	3eqtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) = 𝔸 \cap ℝ$
123		inss2	$⊢ 𝔸 \cap ℝ \subseteq ℝ$
124		aaliou3r	$⊢ \sum_{k \in ℕ} 2^{- k!} \in ℝ$
125		aaliou3	$⊢ \sum_{k \in ℕ} 2^{- k!} \notin 𝔸$
126	125	neli	$⊢ \neg \sum_{k \in ℕ} 2^{- k!} \in 𝔸$
127		elinel1	$⊢ \sum_{k \in ℕ} 2^{- k!} \in (𝔸 \cap ℝ) \to \sum_{k \in ℕ} 2^{- k!} \in 𝔸$
128	126 127	mto	$⊢ \neg \sum_{k \in ℕ} 2^{- k!} \in (𝔸 \cap ℝ)$
129	124 128	pm3.2i	$⊢ (\sum_{k \in ℕ} 2^{- k!} \in ℝ \land \neg \sum_{k \in ℕ} 2^{- k!} \in (𝔸 \cap ℝ))$
130		ssnelpss	$⊢ 𝔸 \cap ℝ \subseteq ℝ \to ((\sum_{k \in ℕ} 2^{- k!} \in ℝ \land \neg \sum_{k \in ℕ} 2^{- k!} \in (𝔸 \cap ℝ)) \to 𝔸 \cap ℝ \subset ℝ)$
131	123 129 130	mp2	$⊢ 𝔸 \cap ℝ \subset ℝ$
132	5	brrpss	$⊢ (𝔸 \cap ℝ) [\subset] ℝ \leftrightarrow 𝔸 \cap ℝ \subset ℝ$
133	131 132	mpbir	$⊢ (𝔸 \cap ℝ) [\subset] ℝ$
134	122 133	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) [\subset] ℝ$
135	134	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) [\subset] ℝ$
136	135	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩) [\subset] ℝ)$
137	6 111 136	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ”⟩ ++ ⟨“ ℝ ”⟩ \in {Chain}_{V} [\subset]$
138	4 137	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ \in {Chain}_{V} [\subset]$
139		s7cli	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ \in Word V$
140		lsw	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ \in Word V \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| - 1)$
141	139 140	ax-mp	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| - 1)$
142		s7len	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| = 7$
143	142	oveq1i	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| - 1 = 7 - 1$
144		7m1e6	$⊢ 7 - 1 = 6$
145	143 144	eqtri	$⊢ \|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| - 1 = 6$
146	145	fveq2i	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (\|⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩\| - 1) = ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (6)$
147	4 112 115	cats1fvn	$⊢ ℝ \in V \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (6) = ℝ$
148	5 147	ax-mp	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ (6) = ℝ$
149	141 146 148	3eqtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) = ℝ$
150	70	simpri	$⊢ (ℚ \subset ℝ \land ℝ \subset ℂ)$
151	150	simpri	$⊢ ℝ \subset ℂ$
152	2	brrpss	$⊢ ℝ [\subset] ℂ \leftrightarrow ℝ \subset ℂ$
153	151 152	mpbir	$⊢ ℝ [\subset] ℂ$
154	149 153	eqbrtri	$⊢ lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) [\subset] ℂ$
155	154	a1i	$⊢ ⊤ \to lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) [\subset] ℂ$
156	155	olcd	$⊢ ⊤ \to (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ = \emptyset \lor lastS (⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩) [\subset] ℂ)$
157	3 138 156	chnccats1	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ”⟩ ++ ⟨“ ℂ ”⟩ \in {Chain}_{V} [\subset]$
158	1 157	eqeltrid	$⊢ ⊤ \to ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ℂ ”⟩ \in {Chain}_{V} [\subset]$
159	158	mptru	$⊢ ⟨“ \{1\} ℕ ℕ_{0} ℤ ℚ (𝔸 \cap ℝ) ℝ ℂ ”⟩ \in {Chain}_{V} [\subset]$

Metamath Proof Explorer

Theorem numtowerdt

Proof