Theorem nthrucw 47335

Description: Some number sets form a chain of proper subsets. This is rephrasing nthruc 16213 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.)

Hypothesis

Ref	Expression
nthrucw.1	⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}

Assertion

Ref	Expression
nthrucw	⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   < (𝑥,𝑦)

Proof of Theorem nthrucw

Dummy variables 𝑎 𝑏 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-s8 14810	. . 3 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩)
2		cnex 11113	. . . . 5 ⊢ ℂ ∈ V
3	2	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ V)
4		df-s7 14809	. . . . 5 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩)
5		reex 11123	. . . . . . 7 ⊢ ℝ ∈ V
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ ∈ V)
7		df-s6 14808	. . . . . . 7 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩)
8	5	inex2 5256	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) ∈ V
9	8	a1i 11	. . . . . . . 8 ⊢ (⊤ → (𝔸 ∩ ℝ) ∈ V)
10		df-s5 14807	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ = (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩)
11		qex 12905	. . . . . . . . . . 11 ⊢ ℚ ∈ V
12	11	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℚ ∈ V)
13		df-s4 14806	. . . . . . . . . . 11 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ = (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩)
14		zex 12527	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
15	14	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ℤ ∈ V)
16		df-s3 14805	. . . . . . . . . . . . 13 ⊢ ⟨“{1}ℕℕ0”⟩ = (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩)
17		nn0ex 12437	. . . . . . . . . . . . . . 15 ⊢ ℕ0 ∈ V
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → ℕ0 ∈ V)
19		df-s2 14804	. . . . . . . . . . . . . . 15 ⊢ ⟨“{1}ℕ”⟩ = (⟨“{1}”⟩ ++ ⟨“ℕ”⟩)
20		nnex 12174	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
21	20	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ℕ ∈ V)
22		snex 5377	. . . . . . . . . . . . . . . . . 18 ⊢ {1} ∈ V
23	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → {1} ∈ V)
24	23	s1chn 18580	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ⟨“{1}”⟩ ∈ ( < Chain V))
25		lsws1 14568	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} ∈ V → (lastS‘⟨“{1}”⟩) = {1})
26	22, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (lastS‘⟨“{1}”⟩) = {1}
27		1nn 12179	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ
28		1ex 11134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ V
29	28	snss 4729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
30	27, 29	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {1} ⊆ ℕ
31		2nn 12248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
32		1re 11138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
33		1lt2 12341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 2
34		ltne 11237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℝ ∧ 1 < 2) → 2 ≠ 1)
35	32, 33, 34	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ≠ 1
36		nelsn 4611	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ≠ 1 → ¬ 2 ∈ {1})
37	35, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 2 ∈ {1}
38	31, 37	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℕ ∧ ¬ 2 ∈ {1})
39		ssnelpss 4055	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({1} ⊆ ℕ → ((2 ∈ ℕ ∧ ¬ 2 ∈ {1}) → {1} ⊊ ℕ))
40	30, 38, 39	mp2 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ {1} ⊊ ℕ
41		psseq1 4031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = {1} → (𝑥 ⊊ 𝑦 ↔ {1} ⊊ 𝑦))
42		psseq2 4032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ℕ → ({1} ⊊ 𝑦 ↔ {1} ⊊ ℕ))
43		nthrucw.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}
44	41, 42, 43	brabg 5488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({1} ∈ V ∧ ℕ ∈ V) → ({1} < ℕ ↔ {1} ⊊ ℕ))
45	22, 20, 44	mp2an 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} < ℕ ↔ {1} ⊊ ℕ)
46	40, 45	mpbir 231	. . . . . . . . . . . . . . . . . . 19 ⊢ {1} < ℕ
47	26, 46	eqbrtri 5107	. . . . . . . . . . . . . . . . . 18 ⊢ (lastS‘⟨“{1}”⟩) < ℕ
48	47	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (lastS‘⟨“{1}”⟩) < ℕ)
49	48	olcd 875	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (⟨“{1}”⟩ = ∅ ∨ (lastS‘⟨“{1}”⟩) < ℕ))
50	21, 24, 49	chnccats1 18585	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (⟨“{1}”⟩ ++ ⟨“ℕ”⟩) ∈ ( < Chain V))
51	19, 50	eqeltrid 2841	. . . . . . . . . . . . . 14 ⊢ (⊤ → ⟨“{1}ℕ”⟩ ∈ ( < Chain V))
52		lsws2 14860	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ∈ V → (lastS‘⟨“{1}ℕ”⟩) = ℕ)
53	20, 52	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (lastS‘⟨“{1}ℕ”⟩) = ℕ
54		nthruz 16214	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ)
55	54	simpli 483	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ ⊊ ℕ0
56		psseq1 4031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ℕ → (𝑥 ⊊ 𝑦 ↔ ℕ ⊊ 𝑦))
57		psseq2 4032	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ℕ0 → (ℕ ⊊ 𝑦 ↔ ℕ ⊊ ℕ0))
58	56, 57, 43	brabg 5488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℕ ∈ V ∧ ℕ0 ∈ V) → (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0))
59	20, 17, 58	mp2an 693	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0)
60	55, 59	mpbir 231	. . . . . . . . . . . . . . . . 17 ⊢ ℕ < ℕ0
61	53, 60	eqbrtri 5107	. . . . . . . . . . . . . . . 16 ⊢ (lastS‘⟨“{1}ℕ”⟩) < ℕ0
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (lastS‘⟨“{1}ℕ”⟩) < ℕ0)
63	62	olcd 875	. . . . . . . . . . . . . 14 ⊢ (⊤ → (⟨“{1}ℕ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕ”⟩) < ℕ0))
64	18, 51, 63	chnccats1 18585	. . . . . . . . . . . . 13 ⊢ (⊤ → (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩) ∈ ( < Chain V))
65	16, 64	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ (⊤ → ⟨“{1}ℕℕ0”⟩ ∈ ( < Chain V))
66		lsws3 14861	. . . . . . . . . . . . . . . 16 ⊢ (ℕ0 ∈ V → (lastS‘⟨“{1}ℕℕ0”⟩) = ℕ0)
67	17, 66	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (lastS‘⟨“{1}ℕℕ0”⟩) = ℕ0
68	54	simpri 485	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ⊊ ℤ
69		psseq1 4031	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ℕ0 → (𝑥 ⊊ 𝑦 ↔ ℕ0 ⊊ 𝑦))
70		psseq2 4032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ℤ → (ℕ0 ⊊ 𝑦 ↔ ℕ0 ⊊ ℤ))
71	69, 70, 43	brabg 5488	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ∈ V ∧ ℤ ∈ V) → (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ))
72	17, 14, 71	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ)
73	68, 72	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ℕ0 < ℤ
74	67, 73	eqbrtri 5107	. . . . . . . . . . . . . 14 ⊢ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ
75	74	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ)
76	75	olcd 875	. . . . . . . . . . . 12 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ))
77	15, 65, 76	chnccats1 18585	. . . . . . . . . . 11 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩) ∈ ( < Chain V))
78	13, 77	eqeltrid 2841	. . . . . . . . . 10 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤ”⟩ ∈ ( < Chain V))
79		lsws4 14862	. . . . . . . . . . . . . 14 ⊢ (ℤ ∈ V → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ)
80	14, 79	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ
81		nthruc 16213	. . . . . . . . . . . . . . . 16 ⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ))
82	81	simpli 483	. . . . . . . . . . . . . . 15 ⊢ (ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ)
83	82	simpri 485	. . . . . . . . . . . . . 14 ⊢ ℤ ⊊ ℚ
84		psseq1 4031	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ℤ → (𝑥 ⊊ 𝑦 ↔ ℤ ⊊ 𝑦))
85		psseq2 4032	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ℚ → (ℤ ⊊ 𝑦 ↔ ℤ ⊊ ℚ))
86	84, 85, 43	brabg 5488	. . . . . . . . . . . . . . 15 ⊢ ((ℤ ∈ V ∧ ℚ ∈ V) → (ℤ < ℚ ↔ ℤ ⊊ ℚ))
87	14, 11, 86	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (ℤ < ℚ ↔ ℤ ⊊ ℚ)
88	83, 87	mpbir 231	. . . . . . . . . . . . 13 ⊢ ℤ < ℚ
89	80, 88	eqbrtri 5107	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ
90	89	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ)
91	90	olcd 875	. . . . . . . . . 10 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ))
92	12, 78, 91	chnccats1 18585	. . . . . . . . 9 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩) ∈ ( < Chain V))
93	10, 92	eqeltrid 2841	. . . . . . . 8 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ ( < Chain V))
94		s5cli 14839	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ Word V
95		lsw 14520	. . . . . . . . . . . . . 14 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩ ∈ Word V → (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = (⟨“{1}ℕℕ0ℤℚ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1)))
96	94, 95	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = (⟨“{1}ℕℕ0ℤℚ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1))
97		s5len 14856	. . . . . . . . . . . . . . . 16 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ”⟩) = 5
98	97	oveq1i 7371	. . . . . . . . . . . . . . 15 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = (5 − 1)
99		5m1e4 12300	. . . . . . . . . . . . . . 15 ⊢ (5 − 1) = 4
100	98, 99	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = 4
101	100	fveq2i 6838	. . . . . . . . . . . . 13 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
102	96, 101	eqtri 2760	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
103		s4cli 14838	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ ∈ Word V
104		s4len 14855	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤ”⟩) = 4
105	10, 103, 104	cats1fvn 14814	. . . . . . . . . . . . 13 ⊢ (ℚ ∈ V → (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ)
106	11, 105	ax-mp 5	. . . . . . . . . . . 12 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ
107	102, 106	eqtri 2760	. . . . . . . . . . 11 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = ℚ
108		qssaa 26304	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ 𝔸
109		qssre 12903	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ ℝ
110	108, 109	ssini 4181	. . . . . . . . . . . . 13 ⊢ ℚ ⊆ (𝔸 ∩ ℝ)
111		2cn 12250	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
112		sqrtcl 15318	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℂ → (√‘2) ∈ ℂ)
113	111, 112	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℂ
114		zsscn 12526	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ⊆ ℂ
115		1z 12551	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℤ
116		2nn0 12448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℕ0
117		plypow 26183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0) → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
118	114, 115, 116, 117	mp3an 1464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ)
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
120		2z 12553	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℤ
121	114, 120	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℤ ⊆ ℂ ∧ 2 ∈ ℤ)
122		plyconst 26184	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℤ ⊆ ℂ ∧ 2 ∈ ℤ) → (ℂ × {2}) ∈ (Poly‘ℤ))
123	121, 122	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℂ × {2}) ∈ (Poly‘ℤ))
124		zaddcl 12561	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ)
125	124	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 + 𝑏) ∈ ℤ)
126		zmulcl 12570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ)
127	126	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑏) ∈ ℤ)
128		neg1z 12557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -1 ∈ ℤ
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → -1 ∈ ℤ)
130	119, 123, 125, 127, 129	plysub 26197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ))
131	130	mptru 1549	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ)
132		0cn 11130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
133		ovex 7394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥↑2) ∈ V
134	133	rgenw 3056	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∀𝑥 ∈ ℂ (𝑥↑2) ∈ V
135		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑥ℂ
136	135	mptfnf 6628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑥 ∈ ℂ (𝑥↑2) ∈ V ↔ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ)
137	134, 136	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ
138		2ex 12252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 ∈ V
139		fconstmpt 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℂ × {2}) = (𝑎 ∈ ℂ ↦ 2)
140	138, 139	fnmpti 6636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℂ × {2}) Fn ℂ
141		fnfvof 7642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ 0 ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
142	137, 140, 141	mpanl12 703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ ∈ V ∧ 0 ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
143	2, 132, 142	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0))
144		oveq1 7368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥↑2) = (0↑2))
145		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) = (𝑥 ∈ ℂ ↦ (𝑥↑2))
146		ovex 7394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0↑2) ∈ V
147	144, 145, 146	fvmpt 6942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2))
148	132, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2)
149		sq0 14148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0↑2) = 0
150	148, 149	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = 0
151	138	fvconst2 7153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℂ → ((ℂ × {2})‘0) = 2)
152	132, 151	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ × {2})‘0) = 2
153	150, 152	oveq12i 7373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)) = (0 − 2)
154	143, 153	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (0 − 2)
155		df-neg 11374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ -2 = (0 − 2)
156	154, 155	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = -2
157		2re 12249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
158	157	renegcli 11449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ -2 ∈ ℝ
159		2pos 12278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
160		lt0neg2 11651	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 ∈ ℝ → (0 < 2 ↔ -2 < 0))
161	157, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 < 2 ↔ -2 < 0)
162	159, 161	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ -2 < 0
163		ltne 11237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-2 ∈ ℝ ∧ -2 < 0) → 0 ≠ -2)
164	158, 162, 163	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≠ -2
165	164	necomi 2987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -2 ≠ 0
166	156, 165	eqnetri 3003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0
167	132, 166	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0)
168		ne0p 26185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0) → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ≠ 0𝑝)
169		nelsn 4611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ≠ 0𝑝 → ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝})
170	167, 168, 169	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝}
171	131, 170	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ) ∧ ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝})
172		eldif 3900	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ↔ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ) ∧ ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝}))
173	171, 172	mpbir 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝})
174		fconstmpt 5687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ × {2}) = (𝑏 ∈ ℂ ↦ 2)
175	138, 174	fnmpti 6636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ × {2}) Fn ℂ
176		fnfvof 7642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ (√‘2) ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
177	137, 175, 176	mpanl12 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ ∈ V ∧ (√‘2) ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
178	2, 113, 177	mp2an 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2)))
179		oveq1 7368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (√‘2) → (𝑥↑2) = ((√‘2)↑2))
180		ovex 7394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((√‘2)↑2) ∈ V
181	179, 145, 180	fvmpt 6942	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((√‘2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2))
182	113, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2)
183		sqrtth 15321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℂ → ((√‘2)↑2) = 2)
184	111, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2)↑2) = 2
185	182, 184	eqtri 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = 2
186	138	fvconst2 7153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2) ∈ ℂ → ((ℂ × {2})‘(√‘2)) = 2)
187	113, 186	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {2})‘(√‘2)) = 2
188	185, 187	oveq12i 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))) = (2 − 2)
189	178, 188	eqtri 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (2 − 2)
190		subid 11407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 ∈ ℂ → (2 − 2) = 0)
191	111, 190	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 2) = 0
192	189, 191	eqtri 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0
193		fveq1 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → (𝑎‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)))
194	193	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → ((𝑎‘(√‘2)) = 0 ↔ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0))
195	194	rspcev 3565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0) → ∃𝑎 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑎‘(√‘2)) = 0)
196		fveq1 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝑎‘(√‘2)) = (𝑥‘(√‘2)))
197	196	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝑎‘(√‘2)) = 0 ↔ (𝑥‘(√‘2)) = 0))
198	197	cbvrexvw 3217	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑎‘(√‘2)) = 0 ↔ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
199	195, 198	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0) → ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
200	173, 192, 199	mp2an 693	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0
201	113, 200	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
202		elaa 26296	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ 𝔸 ↔ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0))
203	201, 202	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ 𝔸
204		sqrt2re 16211	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ ℝ
205	203, 204	elini 4140	. . . . . . . . . . . . . 14 ⊢ (√‘2) ∈ (𝔸 ∩ ℝ)
206		sqrt2irr 16210	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∉ ℚ
207		df-nel 3038	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) ∉ ℚ ↔ ¬ (√‘2) ∈ ℚ)
208	206, 207	mpbi 230	. . . . . . . . . . . . . 14 ⊢ ¬ (√‘2) ∈ ℚ
209	205, 208	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ ((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ)
210		ssnelpss 4055	. . . . . . . . . . . . 13 ⊢ (ℚ ⊆ (𝔸 ∩ ℝ) → (((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ) → ℚ ⊊ (𝔸 ∩ ℝ)))
211	110, 209, 210	mp2 9	. . . . . . . . . . . 12 ⊢ ℚ ⊊ (𝔸 ∩ ℝ)
212		psseq1 4031	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ℚ → (𝑥 ⊊ 𝑦 ↔ ℚ ⊊ 𝑦))
213		psseq2 4032	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝔸 ∩ ℝ) → (ℚ ⊊ 𝑦 ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
214	212, 213, 43	brabg 5488	. . . . . . . . . . . . 13 ⊢ ((ℚ ∈ V ∧ (𝔸 ∩ ℝ) ∈ V) → (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
215	11, 8, 214	mp2an 693	. . . . . . . . . . . 12 ⊢ (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ))
216	211, 215	mpbir 231	. . . . . . . . . . 11 ⊢ ℚ < (𝔸 ∩ ℝ)
217	107, 216	eqbrtri 5107	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)
218	217	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ))
219	218	olcd 875	. . . . . . . 8 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)))
220	9, 93, 219	chnccats1 18585	. . . . . . 7 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩) ∈ ( < Chain V))
221	7, 220	eqeltrid 2841	. . . . . 6 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ ( < Chain V))
222		s6cli 14840	. . . . . . . . . . . 12 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ Word V
223		lsw 14520	. . . . . . . . . . . 12 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ Word V → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1)))
224	222, 223	ax-mp 5	. . . . . . . . . . 11 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1))
225		s6len 14857	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = 6
226	225	oveq1i 7371	. . . . . . . . . . . . 13 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = (6 − 1)
227		6m1e5 12301	. . . . . . . . . . . . 13 ⊢ (6 − 1) = 5
228	226, 227	eqtri 2760	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = 5
229	228	fveq2i 6838	. . . . . . . . . . 11 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
230	224, 229	eqtri 2760	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
231	7, 94, 97	cats1fvn 14814	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ))
232	8, 231	ax-mp 5	. . . . . . . . . 10 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ)
233	230, 232	eqtri 2760	. . . . . . . . 9 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (𝔸 ∩ ℝ)
234		inss2 4179	. . . . . . . . . . 11 ⊢ (𝔸 ∩ ℝ) ⊆ ℝ
235		nnuz 12821	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ≥‘1)
236		1zzd 12552	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℤ)
237		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
238		ovexd 7396	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ V)
239		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑘 → 𝑎 = 𝑘)
240	239	fveq2d 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑘 → (!‘𝑎) = (!‘𝑘))
241	240	negeqd 11381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑘 → -(!‘𝑎) = -(!‘𝑘))
242	241	oveq2d 7377	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑘 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑘)))
243		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
244	242, 243	fvmptg 6940	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ (2↑-(!‘𝑘)) ∈ V) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
245	237, 238, 244	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
246	245	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
247	157	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
248		2ne0 12279	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
249	248	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ≠ 0)
250		nnnn0 12438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
251	250	faccld 14240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (!‘𝑘) ∈ ℕ)
252		nnz 12539	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℕ → (!‘𝑘) ∈ ℤ)
253		znegcl 12556	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℤ → -(!‘𝑘) ∈ ℤ)
254	251, 252, 253	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → -(!‘𝑘) ∈ ℤ)
255	247, 249, 254	reexpclzd 14205	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ ℝ)
256	255	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2↑-(!‘𝑘)) ∈ ℝ)
257		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1)))) = (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1))))
258	257, 243	aaliou3lem3 26324	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ → (seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ≤ (2 · (2↑-(!‘1)))))
259	258	simp1d 1143	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℕ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
260	27, 259	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (⊤ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
261	235, 236, 246, 256, 260	isumrecl 15721	. . . . . . . . . . . . 13 ⊢ (⊤ → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ)
262	261	mptru 1549	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ
263		aaliou3 26331	. . . . . . . . . . . . . 14 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸
264		df-nel 3038	. . . . . . . . . . . . . 14 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸 ↔ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
265	263, 264	mpbi 230	. . . . . . . . . . . . 13 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸
266		elinel1 4142	. . . . . . . . . . . . 13 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ) → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
267	265, 266	mto 197	. . . . . . . . . . . 12 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)
268	262, 267	pm3.2i 470	. . . . . . . . . . 11 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ))
269		ssnelpss 4055	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ⊆ ℝ → ((Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)) → (𝔸 ∩ ℝ) ⊊ ℝ))
270	234, 268, 269	mp2 9	. . . . . . . . . 10 ⊢ (𝔸 ∩ ℝ) ⊊ ℝ
271		psseq1 4031	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝔸 ∩ ℝ) → (𝑥 ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ 𝑦))
272		psseq2 4032	. . . . . . . . . . . 12 ⊢ (𝑦 = ℝ → ((𝔸 ∩ ℝ) ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
273	271, 272, 43	brabg 5488	. . . . . . . . . . 11 ⊢ (((𝔸 ∩ ℝ) ∈ V ∧ ℝ ∈ V) → ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
274	8, 5, 273	mp2an 693	. . . . . . . . . 10 ⊢ ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ)
275	270, 274	mpbir 231	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) < ℝ
276	233, 275	eqbrtri 5107	. . . . . . . 8 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ
277	276	a1i 11	. . . . . . 7 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ)
278	277	olcd 875	. . . . . 6 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ))
279	6, 221, 278	chnccats1 18585	. . . . 5 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩) ∈ ( < Chain V))
280	4, 279	eqeltrid 2841	. . . 4 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ ( < Chain V))
281		s7cli 14841	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ Word V
282		lsw 14520	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ Word V → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)))
283	281, 282	ax-mp 5	. . . . . . . 8 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1))
284		s7len 14858	. . . . . . . . . . . 12 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = 7
285	284	oveq1i 7371	. . . . . . . . . . 11 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = (7 − 1)
286		7m1e6 12302	. . . . . . . . . . 11 ⊢ (7 − 1) = 6
287	285, 286	eqtri 2760	. . . . . . . . . 10 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = 6
288	287	fveq2i 6838	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6)
289	4, 222, 225	cats1fvn 14814	. . . . . . . . . 10 ⊢ (ℝ ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ)
290	5, 289	ax-mp 5	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ
291	288, 290	eqtri 2760	. . . . . . . 8 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = ℝ
292	283, 291	eqtri 2760	. . . . . . 7 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = ℝ
293	81	simpri 485	. . . . . . . . 9 ⊢ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ)
294	293	simpri 485	. . . . . . . 8 ⊢ ℝ ⊊ ℂ
295		psseq1 4031	. . . . . . . . . 10 ⊢ (𝑥 = ℝ → (𝑥 ⊊ 𝑦 ↔ ℝ ⊊ 𝑦))
296		psseq2 4032	. . . . . . . . . 10 ⊢ (𝑦 = ℂ → (ℝ ⊊ 𝑦 ↔ ℝ ⊊ ℂ))
297	295, 296, 43	brabg 5488	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ ℂ ∈ V) → (ℝ < ℂ ↔ ℝ ⊊ ℂ))
298	5, 2, 297	mp2an 693	. . . . . . . 8 ⊢ (ℝ < ℂ ↔ ℝ ⊊ ℂ)
299	294, 298	mpbir 231	. . . . . . 7 ⊢ ℝ < ℂ
300	292, 299	eqbrtri 5107	. . . . . 6 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ
301	300	a1i 11	. . . . 5 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ)
302	301	olcd 875	. . . 4 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ))
303	3, 280, 302	chnccats1 18585	. . 3 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩) ∈ ( < Chain V))
304	1, 303	eqeltrid 2841	. 2 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V))
305	304	mptru 1549	1 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ≠ wne 2933   ∉ wnel 3037  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890   ⊊ wpss 3891  ∅c0 4274  {csn 4568   class class class wbr 5086  {copab 5148   ↦ cmpt 5167   × cxp 5623  dom cdm 5625   Fn wfn 6488  ‘cfv 6493  (class class class)co 7361   ∘_f cof 7623  ℂcc 11030  ℝcr 11031  0cc0 11032  1c1 11033   + caddc 11035   · cmul 11037   < clt 11173   ≤ cle 11174   − cmin 11371  -cneg 11372   / cdiv 11801  ℕcn 12168  2c2 12230  4c4 12232  5c5 12233  6c6 12234  7c7 12235  ℕ₀cn0 12431  ℤcz 12518  ℤ_≥cuz 12782  ℚcq 12892  ℝ⁺crp 12936  seqcseq 13957  ↑cexp 14017  !cfa 14229  ♯chash 14286  Word cword 14469  lastSclsw 14518   ++ cconcat 14526  ⟨“cs1 14552  ⟨“cs2 14797  ⟨“cs3 14798  ⟨“cs4 14799  ⟨“cs5 14800  ⟨“cs6 14801  ⟨“cs7 14802  ⟨“cs8 14803  √csqrt 15189   ⇝ cli 15440  Σcsu 15642   Chain cchn 18565  0_𝑝c0p 25649  Polycply 26162  𝔸caa 26294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-inf2 9556  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110  ax-addf 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7625  df-om 7812  df-1st 7936  df-2nd 7937  df-supp 8105  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-oadd 8403  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-fi 9318  df-sup 9349  df-inf 9350  df-oi 9419  df-dju 9819  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245  df-n0 12432  df-xnn0 12505  df-z 12519  df-dec 12639  df-uz 12783  df-q 12893  df-rp 12937  df-xneg 13057  df-xadd 13058  df-xmul 13059  df-ioo 13296  df-ioc 13297  df-ico 13298  df-icc 13299  df-fz 13456  df-fzo 13603  df-fl 13745  df-mod 13823  df-seq 13958  df-exp 14018  df-fac 14230  df-hash 14287  df-word 14470  df-lsw 14519  df-concat 14527  df-s1 14553  df-s2 14804  df-s3 14805  df-s4 14806  df-s5 14807  df-s6 14808  df-s7 14809  df-s8 14810  df-shft 15023  df-cj 15055  df-re 15056  df-im 15057  df-sqrt 15191  df-abs 15192  df-limsup 15427  df-clim 15444  df-rlim 15445  df-sum 15643  df-struct 17111  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-mulr 17228  df-starv 17229  df-sca 17230  df-vsca 17231  df-ip 17232  df-tset 17233  df-ple 17234  df-ds 17236  df-unif 17237  df-hom 17238  df-cco 17239  df-rest 17379  df-topn 17380  df-0g 17398  df-gsum 17399  df-topgen 17400  df-pt 17401  df-prds 17404  df-xrs 17460  df-qtop 17465  df-imas 17466  df-xps 17468  df-mre 17542  df-mrc 17543  df-acs 17545  df-chn 18566  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-submnd 18746  df-grp 18906  df-minusg 18907  df-mulg 19038  df-subg 19093  df-cntz 19286  df-cmn 19751  df-abl 19752  df-mgp 20116  df-rng 20128  df-ur 20157  df-ring 20210  df-cring 20211  df-subrng 20517  df-subrg 20541  df-psmet 21339  df-xmet 21340  df-met 21341  df-bl 21342  df-mopn 21343  df-fbas 21344  df-fg 21345  df-cnfld 21348  df-top 22872  df-topon 22889  df-topsp 22911  df-bases 22924  df-cld 22997  df-ntr 22998  df-cls 22999  df-nei 23076  df-lp 23114  df-perf 23115  df-cn 23205  df-cnp 23206  df-haus 23293  df-cmp 23365  df-tx 23540  df-hmeo 23733  df-fil 23824  df-fm 23916  df-flim 23917  df-flf 23918  df-xms 24298  df-ms 24299  df-tms 24300  df-cncf 24858  df-0p 25650  df-limc 25846  df-dv 25847  df-dvn 25848  df-cpn 25849  df-ply 26166  df-idp 26167  df-coe 26168  df-dgr 26169  df-quot 26271  df-aa 26295

This theorem is referenced by: (None)