Theorem nthrucw

Description: Some number sets form a chain of proper subsets. This is rephrasing nthruc as a statement about chains; the hypothesis sets the ordering relation to be "is a proper subset". The theorem talks about singleton 1, natural numbers, natural-or-zero numbers, integers, rational numbers, algebraic reals (the definition includes complex numbers as algebraic so intersection is taken), real numbers and complex numbers, which are proper subsets in order. (Contributed by Ender Ting, 29-Jan-2026)

	Ref	Expression
Hypothesis	nthrucw.1	$$⊢\underset{\dot{}}{<}=\left\{⟨x,y⟩|x\subset y\right\}$$
Assertion	nthrucw	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝℂ”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$

Proof

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