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		ltne	$$⊢\left(1\in ℝ\wedge 1<2\right)\to 2\ne 1$$
36	33 34 35	mp2an	$$⊢2\ne 1$$
37		nelsn	$$⊢2\ne 1\to \neg 2\in \left\{1\right\}$$
38	36 37	ax-mp	$$⊢\neg 2\in \left\{1\right\}$$
39	32 38	pm3.2i	$$⊢\left(2\in \mathbb{N}\wedge \neg 2\in \left\{1\right\}\right)$$
40		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)$$
41	31 39 40	mp2	$$⊢\left\{1\right\}\subset \mathbb{N}$$
42		psseq1	$$⊢x=\left\{1\right\}\to \left(x\subset y\leftrightarrow \left\{1\right\}\subset y\right)$$
43		psseq2	$$⊢y=\mathbb{N}\to \left(\left\{1\right\}\subset y\leftrightarrow \left\{1\right\}\subset \mathbb{N}\right)$$
44	42 43 1	brabg	$$⊢\left(\left\{1\right\}\in \mathrm{V}\wedge \mathbb{N}\in \mathrm{V}\right)\to \left(\left\{1\right\}\underset{\dot{}}{<}\mathbb{N}\leftrightarrow \left\{1\right\}\subset \mathbb{N}\right)$$
45	23 21 44	mp2an	$$⊢\left\{1\right\}\underset{\dot{}}{<}\mathbb{N}\leftrightarrow \left\{1\right\}\subset \mathbb{N}$$
46	41 45	mpbir	$$⊢\left\{1\right\}\underset{\dot{}}{<}\mathbb{N}$$
47	27 46	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}”⟩\right)\underset{\dot{}}{<}\mathbb{N}$$
48	47	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}”⟩\right)\underset{\dot{}}{<}\mathbb{N}$$
49	48	olcd	$$⊢\top \to \left(⟨“\left\{1\right\}”⟩=\varnothing \vee \mathrm{lastS}\left(⟨“\left\{1\right\}”⟩\right)\underset{\dot{}}{<}\mathbb{N}\right)$$
50	22 25 49	chnccats1	$$⊢\top \to ⟨“\left\{1\right\}”⟩\mathrm{++}⟨“\mathbb{N}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
51	20 50	eqeltrid	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
52		lsws2	$$⊢\mathbb{N}\in \mathrm{V}\to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}”⟩\right)=\mathbb{N}$$
53	21 52	ax-mp	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}”⟩\right)=\mathbb{N}$$
54		nthruz	$$⊢\left(\mathbb{N}\subset {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subset \mathbb{Z}\right)$$
55	54	simpli	$$⊢\mathbb{N}\subset {\mathbb{N}}_0$$
56		psseq1	$$⊢x=\mathbb{N}\to \left(x\subset y\leftrightarrow \mathbb{N}\subset y\right)$$
57		psseq2	$$⊢y={\mathbb{N}}_0\to \left(\mathbb{N}\subset y\leftrightarrow \mathbb{N}\subset {\mathbb{N}}_0\right)$$
58	56 57 1	brabg	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(\mathbb{N}\underset{\dot{}}{<}{\mathbb{N}}_0\leftrightarrow \mathbb{N}\subset {\mathbb{N}}_0\right)$$
59	21 18 58	mp2an	$$⊢\mathbb{N}\underset{\dot{}}{<}{\mathbb{N}}_0\leftrightarrow \mathbb{N}\subset {\mathbb{N}}_0$$
60	55 59	mpbir	$$⊢\mathbb{N}\underset{\dot{}}{<}{\mathbb{N}}_0$$
61	53 60	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}”⟩\right)\underset{\dot{}}{<}{\mathbb{N}}_0$$
62	61	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}”⟩\right)\underset{\dot{}}{<}{\mathbb{N}}_0$$
63	62	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)$$
64	19 51 63	chnccats1	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}”⟩\mathrm{++}⟨“{\mathbb{N}}_0”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
65	17 64	eqeltrid	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
66		lsws3	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\right)={\mathbb{N}}_0$$
67	18 66	ax-mp	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\right)={\mathbb{N}}_0$$
68	54	simpri	$$⊢{\mathbb{N}}_0\subset \mathbb{Z}$$
69		psseq1	$$⊢x={\mathbb{N}}_0\to \left(x\subset y\leftrightarrow {\mathbb{N}}_0\subset y\right)$$
70		psseq2	$$⊢y=\mathbb{Z}\to \left({\mathbb{N}}_0\subset y\leftrightarrow {\mathbb{N}}_0\subset \mathbb{Z}\right)$$
71	69 70 1	brabg	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \mathbb{Z}\in \mathrm{V}\right)\to \left({\mathbb{N}}_0\underset{\dot{}}{<}\mathbb{Z}\leftrightarrow {\mathbb{N}}_0\subset \mathbb{Z}\right)$$
72	18 15 71	mp2an	$$⊢{\mathbb{N}}_0\underset{\dot{}}{<}\mathbb{Z}\leftrightarrow {\mathbb{N}}_0\subset \mathbb{Z}$$
73	68 72	mpbir	$$⊢{\mathbb{N}}_0\underset{\dot{}}{<}\mathbb{Z}$$
74	67 73	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\right)\underset{\dot{}}{<}\mathbb{Z}$$
75	74	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\right)\underset{\dot{}}{<}\mathbb{Z}$$
76	75	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)$$
77	16 65 76	chnccats1	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0”⟩\mathrm{++}⟨“\mathbb{Z}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
78	14 77	eqeltrid	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
79		lsws4	$$⊢\mathbb{Z}\in \mathrm{V}\to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\right)=\mathbb{Z}$$
80	15 79	ax-mp	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\right)=\mathbb{Z}$$
81		nthruc	$$⊢\left(\left(\mathbb{N}\subset \mathbb{Z}\wedge \mathbb{Z}\subset \mathbb{Q}\right)\wedge \left(\mathbb{Q}\subset ℝ\wedge ℝ\subset ℂ\right)\right)$$
82	81	simpli	$$⊢\left(\mathbb{N}\subset \mathbb{Z}\wedge \mathbb{Z}\subset \mathbb{Q}\right)$$
83	82	simpri	$$⊢\mathbb{Z}\subset \mathbb{Q}$$
84		psseq1	$$⊢x=\mathbb{Z}\to \left(x\subset y\leftrightarrow \mathbb{Z}\subset y\right)$$
85		psseq2	$$⊢y=\mathbb{Q}\to \left(\mathbb{Z}\subset y\leftrightarrow \mathbb{Z}\subset \mathbb{Q}\right)$$
86	84 85 1	brabg	$$⊢\left(\mathbb{Z}\in \mathrm{V}\wedge \mathbb{Q}\in \mathrm{V}\right)\to \left(\mathbb{Z}\underset{\dot{}}{<}\mathbb{Q}\leftrightarrow \mathbb{Z}\subset \mathbb{Q}\right)$$
87	15 12 86	mp2an	$$⊢\mathbb{Z}\underset{\dot{}}{<}\mathbb{Q}\leftrightarrow \mathbb{Z}\subset \mathbb{Q}$$
88	83 87	mpbir	$$⊢\mathbb{Z}\underset{\dot{}}{<}\mathbb{Q}$$
89	80 88	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\right)\underset{\dot{}}{<}\mathbb{Q}$$
90	89	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\right)\underset{\dot{}}{<}\mathbb{Q}$$
91	90	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)$$
92	13 78 91	chnccats1	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\mathrm{++}⟨“\mathbb{Q}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
93	11 92	eqeltrid	$$⊢\top \to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$
94		s5cli	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\in \mathrm{Word}\mathrm{V}$$
95		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)$$
96	94 95	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)$$
97		s5len	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right|=5$$
98	97	oveq1i	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right|-1=5-1$$
99		5m1e4	$$⊢5-1=4$$
100	98 99	eqtri	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right|-1=4$$
101	100	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)$$
102	96 101	eqtri	$$⊢\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(4\right)$$
103		s4cli	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\in \mathrm{Word}\mathrm{V}$$
104		s4len	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}”⟩\right|=4$$
105	11 103 104	cats1fvn	$$⊢\mathbb{Q}\in \mathrm{V}\to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\left(4\right)=\mathbb{Q}$$
106	12 105	ax-mp	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\left(4\right)=\mathbb{Q}$$
107	102 106	eqtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right)=\mathbb{Q}$$
108		qssaa	$$⊢\mathbb{Q}\subseteq 𝔸$$
109		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
110	108 109	ssini	$$⊢\mathbb{Q}\subseteq 𝔸\cap ℝ$$
111		2cn	$$⊢2\in ℂ$$
112		sqrtcl	$$⊢2\in ℂ\to \sqrt{2}\in ℂ$$
113	111 112	ax-mp	$$⊢\sqrt{2}\in ℂ$$
114		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
115		1z	$$⊢1\in \mathbb{Z}$$
116		2nn0	$$⊢2\in {\mathbb{N}}_0$$
117		plypow	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge 1\in \mathbb{Z}\wedge 2\in {\mathbb{N}}_0\right)\to \left(x\in ℂ⟼x^2\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
118	114 115 116 117	mp3an	$$⊢\left(x\in ℂ⟼x^2\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
119	118	a1i	$$⊢\top \to \left(x\in ℂ⟼x^2\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
120		2z	$$⊢2\in \mathbb{Z}$$
121	114 120	pm3.2i	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge 2\in \mathbb{Z}\right)$$
122		plyconst	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge 2\in \mathbb{Z}\right)\to ℂ\times \left\{2\right\}\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
123	121 122	mp1i	$$⊢\top \to ℂ\times \left\{2\right\}\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
124		zaddcl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to a+b\in \mathbb{Z}$$
125	124	adantl	$$⊢\left(\top \wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to a+b\in \mathbb{Z}$$
126		zmulcl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to ab\in \mathbb{Z}$$
127	126	adantl	$$⊢\left(\top \wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to ab\in \mathbb{Z}$$
128		neg1z	$$⊢-1\in \mathbb{Z}$$
129	128	a1i	$$⊢\top \to -1\in \mathbb{Z}$$
130	119 123 125 127 129	plysub	$$⊢\top \to \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
131	130	mptru	$$⊢\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
132		0cn	$$⊢0\in ℂ$$
133		ovex	$$⊢x^2\in \mathrm{V}$$
134	133	rgenw	$$⊢\forall x\in ℂx^2\in \mathrm{V}$$
135		nfcv	$$⊢\underset{\_}{Ⅎ}xℂ$$
136	135	mptfnf	$$⊢\forall x\in ℂx^2\in \mathrm{V}\leftrightarrow \left(x\in ℂ⟼x^2\right)Fnℂ$$
137	134 136	mpbi	$$⊢\left(x\in ℂ⟼x^2\right)Fnℂ$$
138		2ex	$$⊢2\in \mathrm{V}$$
139		fconstmpt	$$⊢ℂ\times \left\{2\right\}=\left(a\in ℂ⟼2\right)$$
140	138 139	fnmpti	$$⊢\left(ℂ\times \left\{2\right\}\right)Fnℂ$$
141		fnfvof	$$⊢\left(\left(\left(x\in ℂ⟼x^2\right)Fnℂ\wedge \left(ℂ\times \left\{2\right\}\right)Fnℂ\right)\wedge \left(ℂ\in \mathrm{V}\wedge 0\in ℂ\right)\right)\to \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)=\left(x\in ℂ⟼x^2\right)\left(0\right)-\left(ℂ\times \left\{2\right\}\right)\left(0\right)$$
142	137 140 141	mpanl12	$$⊢\left(ℂ\in \mathrm{V}\wedge 0\in ℂ\right)\to \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)=\left(x\in ℂ⟼x^2\right)\left(0\right)-\left(ℂ\times \left\{2\right\}\right)\left(0\right)$$
143	3 132 142	mp2an	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)=\left(x\in ℂ⟼x^2\right)\left(0\right)-\left(ℂ\times \left\{2\right\}\right)\left(0\right)$$
144		oveq1	$$⊢x=0\to x^2=0^2$$
145		eqid	$$⊢\left(x\in ℂ⟼x^2\right)=\left(x\in ℂ⟼x^2\right)$$
146		ovex	$$⊢0^2\in \mathrm{V}$$
147	144 145 146	fvmpt	$$⊢0\in ℂ\to \left(x\in ℂ⟼x^2\right)\left(0\right)=0^2$$
148	132 147	ax-mp	$$⊢\left(x\in ℂ⟼x^2\right)\left(0\right)=0^2$$
149		sq0	$$⊢0^2=0$$
150	148 149	eqtri	$$⊢\left(x\in ℂ⟼x^2\right)\left(0\right)=0$$
151	138	fvconst2	$$⊢0\in ℂ\to \left(ℂ\times \left\{2\right\}\right)\left(0\right)=2$$
152	132 151	ax-mp	$$⊢\left(ℂ\times \left\{2\right\}\right)\left(0\right)=2$$
153	150 152	oveq12i	$$⊢\left(x\in ℂ⟼x^2\right)\left(0\right)-\left(ℂ\times \left\{2\right\}\right)\left(0\right)=0-2$$
154	143 153	eqtri	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)=0-2$$
155		df-neg	$$⊢-2=0-2$$
156	154 155	eqtr4i	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)=-2$$
157		2re	$$⊢2\in ℝ$$
158	157	renegcli	$$⊢-2\in ℝ$$
159		2pos	$$⊢0<2$$
160		lt0neg2	$$⊢2\in ℝ\to \left(0<2\leftrightarrow -2<0\right)$$
161	157 160	ax-mp	$$⊢0<2\leftrightarrow -2<0$$
162	159 161	mpbi	$$⊢-2<0$$
163		ltne	$$⊢\left(-2\in ℝ\wedge -2<0\right)\to 0\ne -2$$
164	158 162 163	mp2an	$$⊢0\ne -2$$
165	164	necomi	$$⊢-2\ne 0$$
166	156 165	eqnetri	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)\ne 0$$
167	132 166	pm3.2i	$$⊢\left(0\in ℂ\wedge \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)\ne 0\right)$$
168		ne0p	$$⊢\left(0\in ℂ\wedge \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(0\right)\ne 0\right)\to \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\ne 0_{𝑝}$$
169		nelsn	$$⊢\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\ne 0_{𝑝}\to \neg \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left\{0_{𝑝}\right\}$$
170	167 168 169	mp2b	$$⊢\neg \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left\{0_{𝑝}\right\}$$
171	131 170	pm3.2i	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge \neg \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left\{0_{𝑝}\right\}\right)$$
172		eldif	$$⊢\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\leftrightarrow \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge \neg \left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left\{0_{𝑝}\right\}\right)$$
173	171 172	mpbir	$$⊢\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)$$
174		fconstmpt	$$⊢ℂ\times \left\{2\right\}=\left(b\in ℂ⟼2\right)$$
175	138 174	fnmpti	$$⊢\left(ℂ\times \left\{2\right\}\right)Fnℂ$$
176		fnfvof	$$⊢\left(\left(\left(x\in ℂ⟼x^2\right)Fnℂ\wedge \left(ℂ\times \left\{2\right\}\right)Fnℂ\right)\wedge \left(ℂ\in \mathrm{V}\wedge \sqrt{2}\in ℂ\right)\right)\to \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)-\left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)$$
177	137 175 176	mpanl12	$$⊢\left(ℂ\in \mathrm{V}\wedge \sqrt{2}\in ℂ\right)\to \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)-\left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)$$
178	3 113 177	mp2an	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)-\left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)$$
179		oveq1	$$⊢x=\sqrt{2}\to x^2={\sqrt{2}}^2$$
180		ovex	$$⊢{\sqrt{2}}^2\in \mathrm{V}$$
181	179 145 180	fvmpt	$$⊢\sqrt{2}\in ℂ\to \left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)={\sqrt{2}}^2$$
182	113 181	ax-mp	$$⊢\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)={\sqrt{2}}^2$$
183		sqrtth	$$⊢2\in ℂ\to {\sqrt{2}}^2=2$$
184	111 183	ax-mp	$$⊢{\sqrt{2}}^2=2$$
185	182 184	eqtri	$$⊢\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)=2$$
186	138	fvconst2	$$⊢\sqrt{2}\in ℂ\to \left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)=2$$
187	113 186	ax-mp	$$⊢\left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)=2$$
188	185 187	oveq12i	$$⊢\left(x\in ℂ⟼x^2\right)\left(\sqrt{2}\right)-\left(ℂ\times \left\{2\right\}\right)\left(\sqrt{2}\right)=2-2$$
189	178 188	eqtri	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=2-2$$
190		subid	$$⊢2\in ℂ\to 2-2=0$$
191	111 190	ax-mp	$$⊢2-2=0$$
192	189 191	eqtri	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=0$$
193		fveq1	$$⊢a=\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\to a\left(\sqrt{2}\right)=\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)$$
194	193	eqeq1d	$$⊢a=\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\to \left(a\left(\sqrt{2}\right)=0\leftrightarrow \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=0\right)$$
195	194	rspcev	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=0\right)\to \exists a\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)a\left(\sqrt{2}\right)=0$$
196		fveq1	$$⊢a=x\to a\left(\sqrt{2}\right)=x\left(\sqrt{2}\right)$$
197	196	eqeq1d	$$⊢a=x\to \left(a\left(\sqrt{2}\right)=0\leftrightarrow x\left(\sqrt{2}\right)=0\right)$$
198	197	cbvrexvw	$$⊢\exists a\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)a\left(\sqrt{2}\right)=0\leftrightarrow \exists x\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)x\left(\sqrt{2}\right)=0$$
199	195 198	sylib	$$⊢\left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge \left(\left(x\in ℂ⟼x^2\right){-}_f\left(ℂ\times \left\{2\right\}\right)\right)\left(\sqrt{2}\right)=0\right)\to \exists x\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)x\left(\sqrt{2}\right)=0$$
200	173 192 199	mp2an	$$⊢\exists x\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)x\left(\sqrt{2}\right)=0$$
201	113 200	pm3.2i	$$⊢\left(\sqrt{2}\in ℂ\wedge \exists x\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)x\left(\sqrt{2}\right)=0\right)$$
202		elaa	$$⊢\sqrt{2}\in 𝔸\leftrightarrow \left(\sqrt{2}\in ℂ\wedge \exists x\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)x\left(\sqrt{2}\right)=0\right)$$
203	201 202	mpbir	$$⊢\sqrt{2}\in 𝔸$$
204		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
205	203 204	elini	$$⊢\sqrt{2}\in \left(𝔸\cap ℝ\right)$$
206		sqrt2irr	$$⊢\sqrt{2}\notin \mathbb{Q}$$
207		df-nel	$$⊢\sqrt{2}\notin \mathbb{Q}\leftrightarrow \neg \sqrt{2}\in \mathbb{Q}$$
208	206 207	mpbi	$$⊢\neg \sqrt{2}\in \mathbb{Q}$$
209	205 208	pm3.2i	$$⊢\left(\sqrt{2}\in \left(𝔸\cap ℝ\right)\wedge \neg \sqrt{2}\in \mathbb{Q}\right)$$
210		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)$$
211	110 209 210	mp2	$$⊢\mathbb{Q}\subset 𝔸\cap ℝ$$
212		psseq1	$$⊢x=\mathbb{Q}\to \left(x\subset y\leftrightarrow \mathbb{Q}\subset y\right)$$
213		psseq2	$$⊢y=𝔸\cap ℝ\to \left(\mathbb{Q}\subset y\leftrightarrow \mathbb{Q}\subset 𝔸\cap ℝ\right)$$
214	212 213 1	brabg	$$⊢\left(\mathbb{Q}\in \mathrm{V}\wedge 𝔸\cap ℝ\in \mathrm{V}\right)\to \left(\mathbb{Q}\underset{\dot{}}{<}\left(𝔸\cap ℝ\right)\leftrightarrow \mathbb{Q}\subset 𝔸\cap ℝ\right)$$
215	12 9 214	mp2an	$$⊢\mathbb{Q}\underset{\dot{}}{<}\left(𝔸\cap ℝ\right)\leftrightarrow \mathbb{Q}\subset 𝔸\cap ℝ$$
216	211 215	mpbir	$$⊢\mathbb{Q}\underset{\dot{}}{<}\left(𝔸\cap ℝ\right)$$
217	107 216	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right)\underset{\dot{}}{<}\left(𝔸\cap ℝ\right)$$
218	217	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}”⟩\right)\underset{\dot{}}{<}\left(𝔸\cap ℝ\right)$$
219	218	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)$$
220	10 93 219	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{}}{<}$$
221	8 220	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{}}{<}$$
222		s6cli	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\in \mathrm{Word}\mathrm{V}$$
223		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)$$
224	222 223	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)$$
225		s6len	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right|=6$$
226	225	oveq1i	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right|-1=6-1$$
227		6m1e5	$$⊢6-1=5$$
228	226 227	eqtri	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right|-1=5$$
229	228	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)$$
230	224 229	eqtri	$$⊢\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(5\right)$$
231	8 94 97	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 ℝ$$
232	9 231	ax-mp	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\left(5\right)=𝔸\cap ℝ$$
233	230 232	eqtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right)=𝔸\cap ℝ$$
234		inss2	$$⊢𝔸\cap ℝ\subseteq ℝ$$
235		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
236		1zzd	$$⊢\top \to 1\in \mathbb{Z}$$
237		id	$$⊢k\in \mathbb{N}\to k\in \mathbb{N}$$
238		ovexd	$$⊢k\in \mathbb{N}\to 2^{-k!}\in \mathrm{V}$$
239		id	$$⊢a=k\to a=k$$
240	239	fveq2d	$$⊢a=k\to a!=k!$$
241	240	negeqd	$$⊢a=k\to -a!=-k!$$
242	241	oveq2d	$$⊢a=k\to 2^{-a!}=2^{-k!}$$
243		eqid	$$⊢\left(a\in \mathbb{N}⟼2^{-a!}\right)=\left(a\in \mathbb{N}⟼2^{-a!}\right)$$
244	242 243	fvmptg	$$⊢\left(k\in \mathbb{N}\wedge 2^{-k!}\in \mathrm{V}\right)\to \left(a\in \mathbb{N}⟼2^{-a!}\right)\left(k\right)=2^{-k!}$$
245	237 238 244	syl2anc	$$⊢k\in \mathbb{N}\to \left(a\in \mathbb{N}⟼2^{-a!}\right)\left(k\right)=2^{-k!}$$
246	245	adantl	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to \left(a\in \mathbb{N}⟼2^{-a!}\right)\left(k\right)=2^{-k!}$$
247	157	a1i	$$⊢k\in \mathbb{N}\to 2\in ℝ$$
248		2ne0	$$⊢2\ne 0$$
249	248	a1i	$$⊢k\in \mathbb{N}\to 2\ne 0$$
250		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
251	250	faccld	$$⊢k\in \mathbb{N}\to k!\in \mathbb{N}$$
252		nnz	$$⊢k!\in \mathbb{N}\to k!\in \mathbb{Z}$$
253		znegcl	$$⊢k!\in \mathbb{Z}\to -k!\in \mathbb{Z}$$
254	251 252 253	3syl	$$⊢k\in \mathbb{N}\to -k!\in \mathbb{Z}$$
255	247 249 254	reexpclzd	$$⊢k\in \mathbb{N}\to 2^{-k!}\in ℝ$$
256	255	adantl	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to 2^{-k!}\in ℝ$$
257		eqid	$$⊢\left(n\in {\mathbb{Z}}_{\ge 1}⟼2^{-1!}{\left(\frac{1}{2}\right)}^{n-1}\right)=\left(n\in {\mathbb{Z}}_{\ge 1}⟼2^{-1!}{\left(\frac{1}{2}\right)}^{n-1}\right)$$
258	257 243	aaliou3lem3	$$⊢1\in \mathbb{N}\to \left(seq1\left(+,\left(a\in \mathbb{N}⟼2^{-a!}\right)\right)\in \mathrm{dom}⇝\wedge \sum _{b\in {\mathbb{Z}}_{\ge 1}}\left(a\in \mathbb{N}⟼2^{-a!}\right)\left(b\right)\in {ℝ}^{+}\wedge \sum _{b\in {\mathbb{Z}}_{\ge 1}}\left(a\in \mathbb{N}⟼2^{-a!}\right)\left(b\right)\le 22^{-1!}\right)$$
259	258	simp1d	$$⊢1\in \mathbb{N}\to seq1\left(+,\left(a\in \mathbb{N}⟼2^{-a!}\right)\right)\in \mathrm{dom}⇝$$
260	28 259	mp1i	$$⊢\top \to seq1\left(+,\left(a\in \mathbb{N}⟼2^{-a!}\right)\right)\in \mathrm{dom}⇝$$
261	235 236 246 256 260	isumrecl	$$⊢\top \to \sum _{k\in \mathbb{N}}{2}^{-k!}\in ℝ$$
262	261	mptru	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\in ℝ$$
263		aaliou3	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\notin 𝔸$$
264		df-nel	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\notin 𝔸\leftrightarrow \neg \sum _{k\in \mathbb{N}}{2}^{-k!}\in 𝔸$$
265	263 264	mpbi	$$⊢\neg \sum _{k\in \mathbb{N}}{2}^{-k!}\in 𝔸$$
266		elinel1	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\in \left(𝔸\cap ℝ\right)\to \sum _{k\in \mathbb{N}}{2}^{-k!}\in 𝔸$$
267	265 266	mto	$$⊢\neg \sum _{k\in \mathbb{N}}{2}^{-k!}\in \left(𝔸\cap ℝ\right)$$
268	262 267	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)$$
269		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)$$
270	234 268 269	mp2	$$⊢𝔸\cap ℝ\subset ℝ$$
271		psseq1	$$⊢x=𝔸\cap ℝ\to \left(x\subset y\leftrightarrow 𝔸\cap ℝ\subset y\right)$$
272		psseq2	$$⊢y=ℝ\to \left(𝔸\cap ℝ\subset y\leftrightarrow 𝔸\cap ℝ\subset ℝ\right)$$
273	271 272 1	brabg	$$⊢\left(𝔸\cap ℝ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\to \left(\left(𝔸\cap ℝ\right)\underset{\dot{}}{<}ℝ\leftrightarrow 𝔸\cap ℝ\subset ℝ\right)$$
274	9 6 273	mp2an	$$⊢\left(𝔸\cap ℝ\right)\underset{\dot{}}{<}ℝ\leftrightarrow 𝔸\cap ℝ\subset ℝ$$
275	270 274	mpbir	$$⊢\left(𝔸\cap ℝ\right)\underset{\dot{}}{<}ℝ$$
276	233 275	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right)\underset{\dot{}}{<}ℝ$$
277	276	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)”⟩\right)\underset{\dot{}}{<}ℝ$$
278	277	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)$$
279	7 221 278	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{}}{<}$$
280	5 279	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{}}{<}$$
281		s7cli	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\in \mathrm{Word}\mathrm{V}$$
282		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)$$
283	281 282	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)$$
284		s7len	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right|=7$$
285	284	oveq1i	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right|-1=7-1$$
286		7m1e6	$$⊢7-1=6$$
287	285 286	eqtri	$$⊢\left|⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right|-1=6$$
288	287	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)$$
289	5 222 225	cats1fvn	$$⊢ℝ\in \mathrm{V}\to ⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\left(6\right)=ℝ$$
290	6 289	ax-mp	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\left(6\right)=ℝ$$
291	288 290	eqtri	$$⊢⟨“\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)=ℝ$$
292	283 291	eqtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right)=ℝ$$
293	81	simpri	$$⊢\left(\mathbb{Q}\subset ℝ\wedge ℝ\subset ℂ\right)$$
294	293	simpri	$$⊢ℝ\subset ℂ$$
295		psseq1	$$⊢x=ℝ\to \left(x\subset y\leftrightarrow ℝ\subset y\right)$$
296		psseq2	$$⊢y=ℂ\to \left(ℝ\subset y\leftrightarrow ℝ\subset ℂ\right)$$
297	295 296 1	brabg	$$⊢\left(ℝ\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \left(ℝ\underset{\dot{}}{<}ℂ\leftrightarrow ℝ\subset ℂ\right)$$
298	6 3 297	mp2an	$$⊢ℝ\underset{\dot{}}{<}ℂ\leftrightarrow ℝ\subset ℂ$$
299	294 298	mpbir	$$⊢ℝ\underset{\dot{}}{<}ℂ$$
300	292 299	eqbrtri	$$⊢\mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right)\underset{\dot{}}{<}ℂ$$
301	300	a1i	$$⊢\top \to \mathrm{lastS}\left(⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝ”⟩\right)\underset{\dot{}}{<}ℂ$$
302	301	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)$$
303	4 280 302	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{}}{<}$$
304	2 303	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{}}{<}$$
305	304	mptru	$$⊢⟨“\left\{1\right\}\mathbb{N}{\mathbb{N}}_0\mathbb{Z}\mathbb{Q}\left(𝔸\cap ℝ\right)ℝℂ”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\underset{\dot{}}{<}$$