Metamath Proof Explorer

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 ⊢ < = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }
Assertion nthrucw ⟨“ { 1 } ℕ ℕ0 ℤ ℚ ( 𝔸 ∩ ℝ ) ℝ ℂ ”⟩ ∈ ( < Chain V )

Proof

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