Theorem nthrucw 47493

Description: Some number sets form a chain of proper subsets. This is rephrasing nthruc 16307 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 14890	. . 3 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩)
2		cnex 11180	. . . . 5 ⊢ ℂ ∈ V
3	2	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ V)
4		df-s7 14889	. . . . 5 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩)
5		reex 11190	. . . . . . 7 ⊢ ℝ ∈ V
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ ∈ V)
7		df-s6 14888	. . . . . . 7 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩)
8	5	inex2 5289	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) ∈ V
9	8	a1i 11	. . . . . . . 8 ⊢ (⊤ → (𝔸 ∩ ℝ) ∈ V)
10		df-s5 14887	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ = (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩)
11		qex 12984	. . . . . . . . . . 11 ⊢ ℚ ∈ V
12	11	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℚ ∈ V)
13		df-s4 14886	. . . . . . . . . . 11 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ = (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩)
14		zex 12599	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
15	14	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ℤ ∈ V)
16		df-s3 14885	. . . . . . . . . . . . 13 ⊢ ⟨“{1}ℕℕ0”⟩ = (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩)
17		nn0ex 12509	. . . . . . . . . . . . . . 15 ⊢ ℕ0 ∈ V
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → ℕ0 ∈ V)
19		df-s2 14884	. . . . . . . . . . . . . . 15 ⊢ ⟨“{1}ℕ”⟩ = (⟨“{1}”⟩ ++ ⟨“ℕ”⟩)
20		nnex 12238	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
21	20	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ℕ ∈ V)
22		snex 5411	. . . . . . . . . . . . . . . . . 18 ⊢ {1} ∈ V
23	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → {1} ∈ V)
24	23	s1chn 18675	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ⟨“{1}”⟩ ∈ ( < Chain V))
25		lsws1 14648	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} ∈ V → (lastS‘⟨“{1}”⟩) = {1})
26	22, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (lastS‘⟨“{1}”⟩) = {1}
27		1nn 12243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ
28		1ex 11202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ V
29	28	snss 4755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
30	27, 29	mpbi 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {1} ⊆ ℕ
31		2nn 12313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
32		1re 11207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
33		1lt2 12412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 2
34		ltne 11306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℝ ∧ 1 < 2) → 2 ≠ 1)
35	32, 33, 34	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ≠ 1
36		nelsn 4637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ≠ 1 → ¬ 2 ∈ {1})
37	35, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 2 ∈ {1}
38	31, 37	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℕ ∧ ¬ 2 ∈ {1})
39		ssnelpss 4077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({1} ⊆ ℕ → ((2 ∈ ℕ ∧ ¬ 2 ∈ {1}) → {1} ⊊ ℕ))
40	30, 38, 39	mp2 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ {1} ⊊ ℕ
41		psseq1 4052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = {1} → (𝑥 ⊊ 𝑦 ↔ {1} ⊊ 𝑦))
42		psseq2 4053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ℕ → ({1} ⊊ 𝑦 ↔ {1} ⊊ ℕ))
43		nthrucw.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}
44	41, 42, 43	brabg 5525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({1} ∈ V ∧ ℕ ∈ V) → ({1} < ℕ ↔ {1} ⊊ ℕ))
45	22, 20, 44	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} < ℕ ↔ {1} ⊊ ℕ)
46	40, 45	mpbir 234	. . . . . . . . . . . . . . . . . . 19 ⊢ {1} < ℕ
47	26, 46	eqbrtri 5136	. . . . . . . . . . . . . . . . . 18 ⊢ (lastS‘⟨“{1}”⟩) < ℕ
48	47	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (lastS‘⟨“{1}”⟩) < ℕ)
49	48	olcd 887	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (⟨“{1}”⟩ = ∅ ∨ (lastS‘⟨“{1}”⟩) < ℕ))
50	21, 24, 49	chnccats1 18680	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (⟨“{1}”⟩ ++ ⟨“ℕ”⟩) ∈ ( < Chain V))
51	19, 50	eqeltrid 2873	. . . . . . . . . . . . . 14 ⊢ (⊤ → ⟨“{1}ℕ”⟩ ∈ ( < Chain V))
52		lsws2 14940	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ∈ V → (lastS‘⟨“{1}ℕ”⟩) = ℕ)
53	20, 52	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (lastS‘⟨“{1}ℕ”⟩) = ℕ
54		nthruz 16308	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ)
55	54	simpli 488	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ ⊊ ℕ0
56		psseq1 4052	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ℕ → (𝑥 ⊊ 𝑦 ↔ ℕ ⊊ 𝑦))
57		psseq2 4053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ℕ0 → (ℕ ⊊ 𝑦 ↔ ℕ ⊊ ℕ0))
58	56, 57, 43	brabg 5525	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℕ ∈ V ∧ ℕ0 ∈ V) → (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0))
59	20, 17, 58	mp2an 704	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0)
60	55, 59	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ ℕ < ℕ0
61	53, 60	eqbrtri 5136	. . . . . . . . . . . . . . . 16 ⊢ (lastS‘⟨“{1}ℕ”⟩) < ℕ0
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (lastS‘⟨“{1}ℕ”⟩) < ℕ0)
63	62	olcd 887	. . . . . . . . . . . . . 14 ⊢ (⊤ → (⟨“{1}ℕ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕ”⟩) < ℕ0))
64	18, 51, 63	chnccats1 18680	. . . . . . . . . . . . 13 ⊢ (⊤ → (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩) ∈ ( < Chain V))
65	16, 64	eqeltrid 2873	. . . . . . . . . . . 12 ⊢ (⊤ → ⟨“{1}ℕℕ0”⟩ ∈ ( < Chain V))
66		lsws3 14941	. . . . . . . . . . . . . . . 16 ⊢ (ℕ0 ∈ V → (lastS‘⟨“{1}ℕℕ0”⟩) = ℕ0)
67	17, 66	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (lastS‘⟨“{1}ℕℕ0”⟩) = ℕ0
68	54	simpri 490	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ⊊ ℤ
69		psseq1 4052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ℕ0 → (𝑥 ⊊ 𝑦 ↔ ℕ0 ⊊ 𝑦))
70		psseq2 4053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ℤ → (ℕ0 ⊊ 𝑦 ↔ ℕ0 ⊊ ℤ))
71	69, 70, 43	brabg 5525	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ∈ V ∧ ℤ ∈ V) → (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ))
72	17, 14, 71	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ)
73	68, 72	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ℕ0 < ℤ
74	67, 73	eqbrtri 5136	. . . . . . . . . . . . . 14 ⊢ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ
75	74	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ)
76	75	olcd 887	. . . . . . . . . . . 12 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ))
77	15, 65, 76	chnccats1 18680	. . . . . . . . . . 11 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩) ∈ ( < Chain V))
78	13, 77	eqeltrid 2873	. . . . . . . . . 10 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤ”⟩ ∈ ( < Chain V))
79		lsws4 14942	. . . . . . . . . . . . . 14 ⊢ (ℤ ∈ V → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ)
80	14, 79	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ
81		nthruc 16307	. . . . . . . . . . . . . . . 16 ⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ))
82	81	simpli 488	. . . . . . . . . . . . . . 15 ⊢ (ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ)
83	82	simpri 490	. . . . . . . . . . . . . 14 ⊢ ℤ ⊊ ℚ
84		psseq1 4052	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ℤ → (𝑥 ⊊ 𝑦 ↔ ℤ ⊊ 𝑦))
85		psseq2 4053	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ℚ → (ℤ ⊊ 𝑦 ↔ ℤ ⊊ ℚ))
86	84, 85, 43	brabg 5525	. . . . . . . . . . . . . . 15 ⊢ ((ℤ ∈ V ∧ ℚ ∈ V) → (ℤ < ℚ ↔ ℤ ⊊ ℚ))
87	14, 11, 86	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (ℤ < ℚ ↔ ℤ ⊊ ℚ)
88	83, 87	mpbir 234	. . . . . . . . . . . . 13 ⊢ ℤ < ℚ
89	80, 88	eqbrtri 5136	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ
90	89	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ)
91	90	olcd 887	. . . . . . . . . 10 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ))
92	12, 78, 91	chnccats1 18680	. . . . . . . . 9 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩) ∈ ( < Chain V))
93	10, 92	eqeltrid 2873	. . . . . . . 8 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ ( < Chain V))
94		s5cli 14919	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ Word V
95		lsw 14600	. . . . . . . . . . . . . 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 14936	. . . . . . . . . . . . . . . 16 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ”⟩) = 5
98	97	oveq1i 7421	. . . . . . . . . . . . . . 15 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = (5 − 1)
99		5m1e4 12369	. . . . . . . . . . . . . . 15 ⊢ (5 − 1) = 4
100	98, 99	eqtri 2792	. . . . . . . . . . . . . 14 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = 4
101	100	fveq2i 6885	. . . . . . . . . . . . 13 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
102	96, 101	eqtri 2792	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
103		s4cli 14918	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ ∈ Word V
104		s4len 14935	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤ”⟩) = 4
105	10, 103, 104	cats1fvn 14894	. . . . . . . . . . . . 13 ⊢ (ℚ ∈ V → (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ)
106	11, 105	ax-mp 5	. . . . . . . . . . . 12 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ
107	102, 106	eqtri 2792	. . . . . . . . . . 11 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = ℚ
108		qssaa 26453	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ 𝔸
109		qssre 12982	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ ℝ
110	108, 109	ssini 4200	. . . . . . . . . . . . 13 ⊢ ℚ ⊆ (𝔸 ∩ ℝ)
111		2cn 12315	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
112		sqrtcl 15412	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℂ → (√‘2) ∈ ℂ)
113	111, 112	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℂ
114		zsscn 12598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ⊆ ℂ
115		1z 12623	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℤ
116		2nn0 12520	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℕ0
117		plypow 26330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0) → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
118	114, 115, 116, 117	mp3an 1487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ)
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
120		2z 12625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℤ
121	114, 120	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℤ ⊆ ℂ ∧ 2 ∈ ℤ)
122		plyconst 26331	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℤ ⊆ ℂ ∧ 2 ∈ ℤ) → (ℂ × {2}) ∈ (Poly‘ℤ))
123	121, 122	mp1i 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℂ × {2}) ∈ (Poly‘ℤ))
124		zaddcl 12633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ)
125	124	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 + 𝑏) ∈ ℤ)
126		zmulcl 12642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ)
127	126	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑏) ∈ ℤ)
128		neg1z 12629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -1 ∈ ℤ
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → -1 ∈ ℤ)
130	119, 123, 125, 127, 129	plysub 26344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ))
131	130	mptru 1574	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ)
132		0cn 11197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
133		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥↑2) ∈ V
134	133	rgenw 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∀𝑥 ∈ ℂ (𝑥↑2) ∈ V
135		nfcv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑥ℂ
136	135	mptfnf 6671	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑥 ∈ ℂ (𝑥↑2) ∈ V ↔ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ)
137	134, 136	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ
138		2ex 12317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 ∈ V
139		fconstmpt 5724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℂ × {2}) = (𝑎 ∈ ℂ ↦ 2)
140	138, 139	fnmpti 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℂ × {2}) Fn ℂ
141		fnfvof 7692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ 0 ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
142	137, 140, 141	mpanl12 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ ∈ V ∧ 0 ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
143	2, 132, 142	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0))
144		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥↑2) = (0↑2))
145		eqid 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) = (𝑥 ∈ ℂ ↦ (𝑥↑2))
146		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0↑2) ∈ V
147	144, 145, 146	fvmpt 6990	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2))
148	132, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2)
149		sq0 14227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0↑2) = 0
150	148, 149	eqtri 2792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = 0
151	138	fvconst2 7203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℂ → ((ℂ × {2})‘0) = 2)
152	132, 151	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ × {2})‘0) = 2
153	150, 152	oveq12i 7423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)) = (0 − 2)
154	143, 153	eqtri 2792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (0 − 2)
155		df-neg 11443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ -2 = (0 − 2)
156	154, 155	eqtr4i 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = -2
157		2re 12314	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
158	157	renegcli 11518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ -2 ∈ ℝ
159		2pos 12344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
160		lt0neg2 11720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 ∈ ℝ → (0 < 2 ↔ -2 < 0))
161	157, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 < 2 ↔ -2 < 0)
162	159, 161	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ -2 < 0
163		ltne 11306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-2 ∈ ℝ ∧ -2 < 0) → 0 ≠ -2)
164	158, 162, 163	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≠ -2
165	164	necomi 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -2 ≠ 0
166	156, 165	eqnetri 3034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0
167	132, 166	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0)
168		ne0p 26332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0) → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ≠ 0𝑝)
169		nelsn 4637	. . . . . . . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ) ∧ ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝})
172		eldif 3923	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ↔ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ) ∧ ¬ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ {0𝑝}))
173	171, 172	mpbir 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝})
174		fconstmpt 5724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ × {2}) = (𝑏 ∈ ℂ ↦ 2)
175	138, 174	fnmpti 6679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ × {2}) Fn ℂ
176		fnfvof 7692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ (√‘2) ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
177	137, 175, 176	mpanl12 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ ∈ V ∧ (√‘2) ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
178	2, 113, 177	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2)))
179		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (√‘2) → (𝑥↑2) = ((√‘2)↑2))
180		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((√‘2)↑2) ∈ V
181	179, 145, 180	fvmpt 6990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((√‘2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2))
182	113, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2)
183		sqrtth 15415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℂ → ((√‘2)↑2) = 2)
184	111, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2)↑2) = 2
185	182, 184	eqtri 2792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = 2
186	138	fvconst2 7203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2) ∈ ℂ → ((ℂ × {2})‘(√‘2)) = 2)
187	113, 186	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {2})‘(√‘2)) = 2
188	185, 187	oveq12i 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))) = (2 − 2)
189	178, 188	eqtri 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (2 − 2)
190		subid 11476	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 ∈ ℂ → (2 − 2) = 0)
191	111, 190	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 2) = 0
192	189, 191	eqtri 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0
193		fveq1 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → (𝑎‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)))
194	193	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → ((𝑎‘(√‘2)) = 0 ↔ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0))
195	194	rspcev 3590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0) → ∃𝑎 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑎‘(√‘2)) = 0)
196		fveq1 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝑎‘(√‘2)) = (𝑥‘(√‘2)))
197	196	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝑎‘(√‘2)) = 0 ↔ (𝑥‘(√‘2)) = 0))
198	197	cbvrexvw 3250	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑎‘(√‘2)) = 0 ↔ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
199	195, 198	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0) → ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
200	173, 192, 199	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0
201	113, 200	pm3.2i 475	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
202		elaa 26445	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ 𝔸 ↔ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0))
203	201, 202	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ 𝔸
204		sqrt2re 16305	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ ℝ
205	203, 204	elini 4160	. . . . . . . . . . . . . 14 ⊢ (√‘2) ∈ (𝔸 ∩ ℝ)
206		sqrt2irr 16304	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∉ ℚ
207		df-nel 3071	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) ∉ ℚ ↔ ¬ (√‘2) ∈ ℚ)
208	206, 207	mpbi 233	. . . . . . . . . . . . . 14 ⊢ ¬ (√‘2) ∈ ℚ
209	205, 208	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ ((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ)
210		ssnelpss 4077	. . . . . . . . . . . . 13 ⊢ (ℚ ⊆ (𝔸 ∩ ℝ) → (((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ) → ℚ ⊊ (𝔸 ∩ ℝ)))
211	110, 209, 210	mp2 9	. . . . . . . . . . . 12 ⊢ ℚ ⊊ (𝔸 ∩ ℝ)
212		psseq1 4052	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ℚ → (𝑥 ⊊ 𝑦 ↔ ℚ ⊊ 𝑦))
213		psseq2 4053	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝔸 ∩ ℝ) → (ℚ ⊊ 𝑦 ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
214	212, 213, 43	brabg 5525	. . . . . . . . . . . . 13 ⊢ ((ℚ ∈ V ∧ (𝔸 ∩ ℝ) ∈ V) → (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
215	11, 8, 214	mp2an 704	. . . . . . . . . . . 12 ⊢ (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ))
216	211, 215	mpbir 234	. . . . . . . . . . 11 ⊢ ℚ < (𝔸 ∩ ℝ)
217	107, 216	eqbrtri 5136	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)
218	217	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ))
219	218	olcd 887	. . . . . . . 8 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)))
220	9, 93, 219	chnccats1 18680	. . . . . . 7 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩) ∈ ( < Chain V))
221	7, 220	eqeltrid 2873	. . . . . 6 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ ( < Chain V))
222		s6cli 14920	. . . . . . . . . . . 12 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ Word V
223		lsw 14600	. . . . . . . . . . . 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 14937	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = 6
226	225	oveq1i 7421	. . . . . . . . . . . . 13 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = (6 − 1)
227		6m1e5 12370	. . . . . . . . . . . . 13 ⊢ (6 − 1) = 5
228	226, 227	eqtri 2792	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = 5
229	228	fveq2i 6885	. . . . . . . . . . 11 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
230	224, 229	eqtri 2792	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
231	7, 94, 97	cats1fvn 14894	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ))
232	8, 231	ax-mp 5	. . . . . . . . . 10 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ)
233	230, 232	eqtri 2792	. . . . . . . . 9 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (𝔸 ∩ ℝ)
234		inss2 4198	. . . . . . . . . . 11 ⊢ (𝔸 ∩ ℝ) ⊆ ℝ
235		nnuz 12900	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ≥‘1)
236		1zzd 12624	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℤ)
237		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
238		ovexd 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ V)
239		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑘 → 𝑎 = 𝑘)
240	239	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑘 → (!‘𝑎) = (!‘𝑘))
241	240	negeqd 11450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑘 → -(!‘𝑎) = -(!‘𝑘))
242	241	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑘 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑘)))
243		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
244	242, 243	fvmptg 6988	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ (2↑-(!‘𝑘)) ∈ V) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
245	237, 238, 244	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
246	245	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
247	157	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
248		2ne0 12346	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
249	248	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ≠ 0)
250		nnnn0 12510	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
251	250	faccld 14319	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (!‘𝑘) ∈ ℕ)
252		nnz 12611	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℕ → (!‘𝑘) ∈ ℤ)
253		znegcl 12628	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℤ → -(!‘𝑘) ∈ ℤ)
254	251, 252, 253	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → -(!‘𝑘) ∈ ℤ)
255	247, 249, 254	reexpclzd 14284	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ ℝ)
256	255	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2↑-(!‘𝑘)) ∈ ℝ)
257		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1)))) = (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1))))
258	257, 243	aaliou3lem3 26473	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ → (seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ≤ (2 · (2↑-(!‘1)))))
259	258	simp1d 1158	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℕ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
260	27, 259	mp1i 14	. . . . . . . . . . . . . 14 ⊢ (⊤ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
261	235, 236, 246, 256, 260	isumrecl 15815	. . . . . . . . . . . . 13 ⊢ (⊤ → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ)
262	261	mptru 1574	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ
263		aaliou3 26480	. . . . . . . . . . . . . 14 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸
264		df-nel 3071	. . . . . . . . . . . . . 14 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸 ↔ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
265	263, 264	mpbi 233	. . . . . . . . . . . . 13 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸
266		elinel1 4162	. . . . . . . . . . . . 13 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ) → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
267	265, 266	mto 200	. . . . . . . . . . . 12 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)
268	262, 267	pm3.2i 475	. . . . . . . . . . 11 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ))
269		ssnelpss 4077	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ⊆ ℝ → ((Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)) → (𝔸 ∩ ℝ) ⊊ ℝ))
270	234, 268, 269	mp2 9	. . . . . . . . . 10 ⊢ (𝔸 ∩ ℝ) ⊊ ℝ
271		psseq1 4052	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝔸 ∩ ℝ) → (𝑥 ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ 𝑦))
272		psseq2 4053	. . . . . . . . . . . 12 ⊢ (𝑦 = ℝ → ((𝔸 ∩ ℝ) ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
273	271, 272, 43	brabg 5525	. . . . . . . . . . 11 ⊢ (((𝔸 ∩ ℝ) ∈ V ∧ ℝ ∈ V) → ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
274	8, 5, 273	mp2an 704	. . . . . . . . . 10 ⊢ ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ)
275	270, 274	mpbir 234	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) < ℝ
276	233, 275	eqbrtri 5136	. . . . . . . 8 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ
277	276	a1i 11	. . . . . . 7 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ)
278	277	olcd 887	. . . . . 6 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ))
279	6, 221, 278	chnccats1 18680	. . . . 5 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩) ∈ ( < Chain V))
280	4, 279	eqeltrid 2873	. . . 4 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ ( < Chain V))
281		s7cli 14921	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ Word V
282		lsw 14600	. . . . . . . . 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 14938	. . . . . . . . . . . 12 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = 7
285	284	oveq1i 7421	. . . . . . . . . . 11 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = (7 − 1)
286		7m1e6 12371	. . . . . . . . . . 11 ⊢ (7 − 1) = 6
287	285, 286	eqtri 2792	. . . . . . . . . 10 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = 6
288	287	fveq2i 6885	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6)
289	4, 222, 225	cats1fvn 14894	. . . . . . . . . 10 ⊢ (ℝ ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ)
290	5, 289	ax-mp 5	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ
291	288, 290	eqtri 2792	. . . . . . . 8 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = ℝ
292	283, 291	eqtri 2792	. . . . . . 7 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = ℝ
293	81	simpri 490	. . . . . . . . 9 ⊢ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ)
294	293	simpri 490	. . . . . . . 8 ⊢ ℝ ⊊ ℂ
295		psseq1 4052	. . . . . . . . . 10 ⊢ (𝑥 = ℝ → (𝑥 ⊊ 𝑦 ↔ ℝ ⊊ 𝑦))
296		psseq2 4053	. . . . . . . . . 10 ⊢ (𝑦 = ℂ → (ℝ ⊊ 𝑦 ↔ ℝ ⊊ ℂ))
297	295, 296, 43	brabg 5525	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ ℂ ∈ V) → (ℝ < ℂ ↔ ℝ ⊊ ℂ))
298	5, 2, 297	mp2an 704	. . . . . . . 8 ⊢ (ℝ < ℂ ↔ ℝ ⊊ ℂ)
299	294, 298	mpbir 234	. . . . . . 7 ⊢ ℝ < ℂ
300	292, 299	eqbrtri 5136	. . . . . 6 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ
301	300	a1i 11	. . . . 5 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ)
302	301	olcd 887	. . . 4 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ))
303	3, 280, 302	chnccats1 18680	. . 3 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩) ∈ ( < Chain V))
304	1, 303	eqeltrid 2873	. 2 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V))
305	304	mptru 1574	1 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149   ≠ wne 2964   ∉ wnel 3070  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∖ cdif 3910   ∩ cin 3912   ⊆ wss 3913   ⊊ wpss 3914  ∅c0 4294  {csn 4594   class class class wbr 5113  {copab 5177   ↦ cmpt 5196   × cxp 5660  dom cdm 5662   Fn wfn 6532  ‘cfv 6537  (class class class)co 7411   ∘_f cof 7673  ℂcc 11097  ℝcr 11098  0cc0 11099  1c1 11100   + caddc 11102   · cmul 11104   < clt 11242   ≤ cle 11243   − cmin 11440  -cneg 11441   / cdiv 11870  ℕcn 12232  2c2 12294  4c4 12296  5c5 12297  6c6 12298  7c7 12299  ℕ₀cn0 12503  ℤcz 12590  ℤ_≥cuz 12861  ℚcq 12971  ℝ⁺crp 13015  seqcseq 14036  ↑cexp 14096  !cfa 14308  ♯chash 14365  Word cword 14549  lastSclsw 14598   ++ cconcat 14606  ⟨“cs1 14632  ⟨“cs2 14877  ⟨“cs3 14878  ⟨“cs4 14879  ⟨“cs5 14880  ⟨“cs6 14881  ⟨“cs7 14882  ⟨“cs8 14883  √csqrt 15283   ⇝ cli 15534  Σcsu 15736   Chain cchn 18660  0_𝑝c0p 25796  Polycply 26309  𝔸caa 26443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-inf2 9609  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177  ax-addf 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-om 7862  df-1st 7985  df-2nd 7986  df-supp 8156  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-oadd 8456  df-er 8693  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9321  df-fi 9370  df-sup 9401  df-inf 9402  df-oi 9471  df-dju 9886  df-card 9924  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-xnn0 12577  df-z 12591  df-dec 12711  df-uz 12862  df-q 12972  df-rp 13016  df-xneg 13136  df-xadd 13137  df-xmul 13138  df-ioo 13375  df-ioc 13376  df-ico 13377  df-icc 13378  df-fz 13535  df-fzo 13682  df-fl 13824  df-mod 13902  df-seq 14037  df-exp 14097  df-fac 14309  df-hash 14366  df-word 14550  df-lsw 14599  df-concat 14607  df-s1 14633  df-s2 14884  df-s3 14885  df-s4 14886  df-s5 14887  df-s6 14888  df-s7 14889  df-s8 14890  df-shft 15103  df-cj 15149  df-re 15150  df-im 15151  df-sqrt 15285  df-abs 15286  df-limsup 15521  df-clim 15538  df-rlim 15539  df-sum 15737  df-struct 17206  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-mulr 17323  df-starv 17324  df-sca 17325  df-vsca 17326  df-ip 17327  df-tset 17328  df-ple 17329  df-ds 17331  df-unif 17332  df-hom 17333  df-cco 17334  df-rest 17474  df-topn 17475  df-0g 17493  df-gsum 17494  df-topgen 17495  df-pt 17496  df-prds 17499  df-xrs 17555  df-qtop 17560  df-imas 17561  df-xps 17563  df-mre 17637  df-mrc 17638  df-acs 17640  df-chn 18661  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-submnd 18841  df-grp 19002  df-minusg 19003  df-mulg 19133  df-subg 19188  df-cntz 19386  df-cmn 19851  df-abl 19852  df-mgp 20216  df-rng 20230  df-ur 20263  df-ring 20316  df-cring 20317  df-subrng 20630  df-subrg 20654  df-psmet 21482  df-xmet 21483  df-met 21484  df-bl 21485  df-mopn 21486  df-fbas 21487  df-fg 21488  df-cnfld 21491  df-top 23019  df-topon 23036  df-topsp 23058  df-bases 23071  df-cld 23144  df-ntr 23145  df-cls 23146  df-nei 23223  df-lp 23261  df-perf 23262  df-cn 23352  df-cnp 23353  df-haus 23440  df-cmp 23512  df-tx 23687  df-hmeo 23880  df-fil 23971  df-fm 24063  df-flim 24064  df-flf 24065  df-xms 24445  df-ms 24446  df-tms 24447  df-cncf 25005  df-0p 25797  df-limc 25993  df-dv 25994  df-dvn 25995  df-cpn 25996  df-ply 26313  df-idp 26314  df-coe 26315  df-dgr 26316  df-quot 26420  df-aa 26444

This theorem is referenced by: (None)