Metamath Proof Explorer

Theorem 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 ℤ ℚ ( 𝔸 ∩ ℝ ) ℝ ℂ ”⟩ ∈ ( [⊊] Chain V )

Proof

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