Theorem nthrucw 46994

Description: Some number sets form a chain of proper subsets. This is rephrasing nthruc 16161 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 14761	. . 3 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩)
2		cnex 11087	. . . . 5 ⊢ ℂ ∈ V
3	2	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ V)
4		df-s7 14760	. . . . 5 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩)
5		reex 11097	. . . . . . 7 ⊢ ℝ ∈ V
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ ∈ V)
7		df-s6 14759	. . . . . . 7 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩)
8	5	inex2 5254	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) ∈ V
9	8	a1i 11	. . . . . . . 8 ⊢ (⊤ → (𝔸 ∩ ℝ) ∈ V)
10		df-s5 14758	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ = (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩)
11		qex 12859	. . . . . . . . . . 11 ⊢ ℚ ∈ V
12	11	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℚ ∈ V)
13		df-s4 14757	. . . . . . . . . . 11 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ = (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩)
14		zex 12477	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
15	14	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ℤ ∈ V)
16		df-s3 14756	. . . . . . . . . . . . 13 ⊢ ⟨“{1}ℕℕ0”⟩ = (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩)
17		nn0ex 12387	. . . . . . . . . . . . . . 15 ⊢ ℕ0 ∈ V
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → ℕ0 ∈ V)
19		df-s2 14755	. . . . . . . . . . . . . . 15 ⊢ ⟨“{1}ℕ”⟩ = (⟨“{1}”⟩ ++ ⟨“ℕ”⟩)
20		nnex 12131	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
21	20	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ℕ ∈ V)
22		snex 5372	. . . . . . . . . . . . . . . . . 18 ⊢ {1} ∈ V
23	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → {1} ∈ V)
24	23	s1chn 18526	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ⟨“{1}”⟩ ∈ ( < Chain V))
25		lsws1 14519	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} ∈ V → (lastS‘⟨“{1}”⟩) = {1})
26	22, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (lastS‘⟨“{1}”⟩) = {1}
27		1nn 12136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ
28		1ex 11108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ V
29	28	snss 4734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
30	27, 29	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {1} ⊆ ℕ
31		2nn 12198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
32		1re 11112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
33		1lt2 12291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 2
34		ltne 11210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℝ ∧ 1 < 2) → 2 ≠ 1)
35	32, 33, 34	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ≠ 1
36		nelsn 4616	. . . . . . . . . . . . . . . . . . . . . . 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 4061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({1} ⊆ ℕ → ((2 ∈ ℕ ∧ ¬ 2 ∈ {1}) → {1} ⊊ ℕ))
40	30, 38, 39	mp2 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ {1} ⊊ ℕ
41		psseq1 4037	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = {1} → (𝑥 ⊊ 𝑦 ↔ {1} ⊊ 𝑦))
42		psseq2 4038	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ℕ → ({1} ⊊ 𝑦 ↔ {1} ⊊ ℕ))
43		nthrucw.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}
44	41, 42, 43	brabg 5477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({1} ∈ V ∧ ℕ ∈ V) → ({1} < ℕ ↔ {1} ⊊ ℕ))
45	22, 20, 44	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({1} < ℕ ↔ {1} ⊊ ℕ)
46	40, 45	mpbir 231	. . . . . . . . . . . . . . . . . . 19 ⊢ {1} < ℕ
47	26, 46	eqbrtri 5110	. . . . . . . . . . . . . . . . . 18 ⊢ (lastS‘⟨“{1}”⟩) < ℕ
48	47	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (lastS‘⟨“{1}”⟩) < ℕ)
49	48	olcd 874	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (⟨“{1}”⟩ = ∅ ∨ (lastS‘⟨“{1}”⟩) < ℕ))
50	21, 24, 49	chnccats1 18531	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (⟨“{1}”⟩ ++ ⟨“ℕ”⟩) ∈ ( < Chain V))
51	19, 50	eqeltrid 2835	. . . . . . . . . . . . . 14 ⊢ (⊤ → ⟨“{1}ℕ”⟩ ∈ ( < Chain V))
52		lsws2 14811	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ ∈ V → (lastS‘⟨“{1}ℕ”⟩) = ℕ)
53	20, 52	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (lastS‘⟨“{1}ℕ”⟩) = ℕ
54		nthruz 16162	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ)
55	54	simpli 483	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ ⊊ ℕ0
56		psseq1 4037	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ℕ → (𝑥 ⊊ 𝑦 ↔ ℕ ⊊ 𝑦))
57		psseq2 4038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ℕ0 → (ℕ ⊊ 𝑦 ↔ ℕ ⊊ ℕ0))
58	56, 57, 43	brabg 5477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℕ ∈ V ∧ ℕ0 ∈ V) → (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0))
59	20, 17, 58	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ (ℕ < ℕ0 ↔ ℕ ⊊ ℕ0)
60	55, 59	mpbir 231	. . . . . . . . . . . . . . . . 17 ⊢ ℕ < ℕ0
61	53, 60	eqbrtri 5110	. . . . . . . . . . . . . . . 16 ⊢ (lastS‘⟨“{1}ℕ”⟩) < ℕ0
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (lastS‘⟨“{1}ℕ”⟩) < ℕ0)
63	62	olcd 874	. . . . . . . . . . . . . 14 ⊢ (⊤ → (⟨“{1}ℕ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕ”⟩) < ℕ0))
64	18, 51, 63	chnccats1 18531	. . . . . . . . . . . . 13 ⊢ (⊤ → (⟨“{1}ℕ”⟩ ++ ⟨“ℕ0”⟩) ∈ ( < Chain V))
65	16, 64	eqeltrid 2835	. . . . . . . . . . . 12 ⊢ (⊤ → ⟨“{1}ℕℕ0”⟩ ∈ ( < Chain V))
66		lsws3 14812	. . . . . . . . . . . . . . . 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 4037	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ℕ0 → (𝑥 ⊊ 𝑦 ↔ ℕ0 ⊊ 𝑦))
70		psseq2 4038	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ℤ → (ℕ0 ⊊ 𝑦 ↔ ℕ0 ⊊ ℤ))
71	69, 70, 43	brabg 5477	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ∈ V ∧ ℤ ∈ V) → (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ))
72	17, 14, 71	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (ℕ0 < ℤ ↔ ℕ0 ⊊ ℤ)
73	68, 72	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ℕ0 < ℤ
74	67, 73	eqbrtri 5110	. . . . . . . . . . . . . 14 ⊢ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ
75	74	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ)
76	75	olcd 874	. . . . . . . . . . . 12 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0”⟩) < ℤ))
77	15, 65, 76	chnccats1 18531	. . . . . . . . . . 11 ⊢ (⊤ → (⟨“{1}ℕℕ0”⟩ ++ ⟨“ℤ”⟩) ∈ ( < Chain V))
78	13, 77	eqeltrid 2835	. . . . . . . . . 10 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤ”⟩ ∈ ( < Chain V))
79		lsws4 14813	. . . . . . . . . . . . . 14 ⊢ (ℤ ∈ V → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ)
80	14, 79	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) = ℤ
81		nthruc 16161	. . . . . . . . . . . . . . . 16 ⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ))
82	81	simpli 483	. . . . . . . . . . . . . . 15 ⊢ (ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ)
83	82	simpri 485	. . . . . . . . . . . . . 14 ⊢ ℤ ⊊ ℚ
84		psseq1 4037	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ℤ → (𝑥 ⊊ 𝑦 ↔ ℤ ⊊ 𝑦))
85		psseq2 4038	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ℚ → (ℤ ⊊ 𝑦 ↔ ℤ ⊊ ℚ))
86	84, 85, 43	brabg 5477	. . . . . . . . . . . . . . 15 ⊢ ((ℤ ∈ V ∧ ℚ ∈ V) → (ℤ < ℚ ↔ ℤ ⊊ ℚ))
87	14, 11, 86	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (ℤ < ℚ ↔ ℤ ⊊ ℚ)
88	83, 87	mpbir 231	. . . . . . . . . . . . 13 ⊢ ℤ < ℚ
89	80, 88	eqbrtri 5110	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ
90	89	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ)
91	90	olcd 874	. . . . . . . . . 10 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤ”⟩) < ℚ))
92	12, 78, 91	chnccats1 18531	. . . . . . . . 9 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤ”⟩ ++ ⟨“ℚ”⟩) ∈ ( < Chain V))
93	10, 92	eqeltrid 2835	. . . . . . . 8 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ ( < Chain V))
94		s5cli 14790	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤℚ”⟩ ∈ Word V
95		lsw 14471	. . . . . . . . . . . . . 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 14807	. . . . . . . . . . . . . . . 16 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ”⟩) = 5
98	97	oveq1i 7356	. . . . . . . . . . . . . . 15 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = (5 − 1)
99		5m1e4 12250	. . . . . . . . . . . . . . 15 ⊢ (5 − 1) = 4
100	98, 99	eqtri 2754	. . . . . . . . . . . . . 14 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1) = 4
101	100	fveq2i 6825	. . . . . . . . . . . . 13 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
102	96, 101	eqtri 2754	. . . . . . . . . . . 12 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = (⟨“{1}ℕℕ0ℤℚ”⟩‘4)
103		s4cli 14789	. . . . . . . . . . . . . 14 ⊢ ⟨“{1}ℕℕ0ℤ”⟩ ∈ Word V
104		s4len 14806	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤ”⟩) = 4
105	10, 103, 104	cats1fvn 14765	. . . . . . . . . . . . 13 ⊢ (ℚ ∈ V → (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ)
106	11, 105	ax-mp 5	. . . . . . . . . . . 12 ⊢ (⟨“{1}ℕℕ0ℤℚ”⟩‘4) = ℚ
107	102, 106	eqtri 2754	. . . . . . . . . . 11 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) = ℚ
108		qssaa 26259	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ 𝔸
109		qssre 12857	. . . . . . . . . . . . . 14 ⊢ ℚ ⊆ ℝ
110	108, 109	ssini 4187	. . . . . . . . . . . . 13 ⊢ ℚ ⊆ (𝔸 ∩ ℝ)
111		2cn 12200	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
112		sqrtcl 15269	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℂ → (√‘2) ∈ ℂ)
113	111, 112	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℂ
114		zsscn 12476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ⊆ ℂ
115		1z 12502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℤ
116		2nn0 12398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℕ0
117		plypow 26137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0) → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
118	114, 115, 116, 117	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ)
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℤ))
120		2z 12504	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℤ
121	114, 120	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℤ ⊆ ℂ ∧ 2 ∈ ℤ)
122		plyconst 26138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℤ ⊆ ℂ ∧ 2 ∈ ℤ) → (ℂ × {2}) ∈ (Poly‘ℤ))
123	121, 122	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℂ × {2}) ∈ (Poly‘ℤ))
124		zaddcl 12512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ)
125	124	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 + 𝑏) ∈ ℤ)
126		zmulcl 12521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ)
127	126	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑏) ∈ ℤ)
128		neg1z 12508	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -1 ∈ ℤ
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → -1 ∈ ℤ)
130	119, 123, 125, 127, 129	plysub 26151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ))
131	130	mptru 1548	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ (Poly‘ℤ)
132		0cn 11104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℂ
133		ovex 7379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥↑2) ∈ V
134	133	rgenw 3051	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∀𝑥 ∈ ℂ (𝑥↑2) ∈ V
135		nfcv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑥ℂ
136	135	mptfnf 6616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑥 ∈ ℂ (𝑥↑2) ∈ V ↔ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ)
137	134, 136	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ
138		2ex 12202	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 ∈ V
139		fconstmpt 5676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℂ × {2}) = (𝑎 ∈ ℂ ↦ 2)
140	138, 139	fnmpti 6624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℂ × {2}) Fn ℂ
141		fnfvof 7627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ 0 ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
142	137, 140, 141	mpanl12 702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ ∈ V ∧ 0 ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)))
143	2, 132, 142	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0))
144		oveq1 7353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥↑2) = (0↑2))
145		eqid 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) = (𝑥 ∈ ℂ ↦ (𝑥↑2))
146		ovex 7379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0↑2) ∈ V
147	144, 145, 146	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2))
148	132, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = (0↑2)
149		sq0 14099	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0↑2) = 0
150	148, 149	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) = 0
151	138	fvconst2 7138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℂ → ((ℂ × {2})‘0) = 2)
152	132, 151	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℂ × {2})‘0) = 2
153	150, 152	oveq12i 7358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘0) − ((ℂ × {2})‘0)) = (0 − 2)
154	143, 153	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = (0 − 2)
155		df-neg 11347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ -2 = (0 − 2)
156	154, 155	eqtr4i 2757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) = -2
157		2re 12199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
158	157	renegcli 11422	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ -2 ∈ ℝ
159		2pos 12228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
160		lt0neg2 11624	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 11210	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((-2 ∈ ℝ ∧ -2 < 0) → 0 ≠ -2)
164	158, 162, 163	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≠ -2
165	164	necomi 2982	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -2 ≠ 0
166	156, 165	eqnetri 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0
167	132, 166	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0)
168		ne0p 26139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℂ ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘0) ≠ 0) → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ≠ 0𝑝)
169		nelsn 4616	. . . . . . . . . . . . . . . . . . . . 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 3907	. . . . . . . . . . . . . . . . . . 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 5676	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ × {2}) = (𝑏 ∈ ℂ ↦ 2)
175	138, 174	fnmpti 6624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ × {2}) Fn ℂ
176		fnfvof 7627	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ (ℂ × {2}) Fn ℂ) ∧ (ℂ ∈ V ∧ (√‘2) ∈ ℂ)) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
177	137, 175, 176	mpanl12 702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ ∈ V ∧ (√‘2) ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))))
178	2, 113, 177	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2)))
179		oveq1 7353	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (√‘2) → (𝑥↑2) = ((√‘2)↑2))
180		ovex 7379	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((√‘2)↑2) ∈ V
181	179, 145, 180	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((√‘2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2))
182	113, 181	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = ((√‘2)↑2)
183		sqrtth 15272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℂ → ((√‘2)↑2) = 2)
184	111, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2)↑2) = 2
185	182, 184	eqtri 2754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) = 2
186	138	fvconst2 7138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((√‘2) ∈ ℂ → ((ℂ × {2})‘(√‘2)) = 2)
187	113, 186	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ × {2})‘(√‘2)) = 2
188	185, 187	oveq12i 7358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘2)) − ((ℂ × {2})‘(√‘2))) = (2 − 2)
189	178, 188	eqtri 2754	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = (2 − 2)
190		subid 11380	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 ∈ ℂ → (2 − 2) = 0)
191	111, 190	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 2) = 0
192	189, 191	eqtri 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0
193		fveq1 6821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → (𝑎‘(√‘2)) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)))
194	193	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) → ((𝑎‘(√‘2)) = 0 ↔ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0))
195	194	rspcev 3572	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2})) ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘f − (ℂ × {2}))‘(√‘2)) = 0) → ∃𝑎 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑎‘(√‘2)) = 0)
196		fveq1 6821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝑎‘(√‘2)) = (𝑥‘(√‘2)))
197	196	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝑎‘(√‘2)) = 0 ↔ (𝑥‘(√‘2)) = 0))
198	197	cbvrexvw 3211	. . . . . . . . . . . . . . . . . . 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 692	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0
201	113, 200	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0)
202		elaa 26251	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ 𝔸 ↔ ((√‘2) ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑥‘(√‘2)) = 0))
203	201, 202	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ 𝔸
204		sqrt2re 16159	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∈ ℝ
205	203, 204	elini 4146	. . . . . . . . . . . . . 14 ⊢ (√‘2) ∈ (𝔸 ∩ ℝ)
206		sqrt2irr 16158	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ∉ ℚ
207		df-nel 3033	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) ∉ ℚ ↔ ¬ (√‘2) ∈ ℚ)
208	206, 207	mpbi 230	. . . . . . . . . . . . . 14 ⊢ ¬ (√‘2) ∈ ℚ
209	205, 208	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ ((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ)
210		ssnelpss 4061	. . . . . . . . . . . . 13 ⊢ (ℚ ⊆ (𝔸 ∩ ℝ) → (((√‘2) ∈ (𝔸 ∩ ℝ) ∧ ¬ (√‘2) ∈ ℚ) → ℚ ⊊ (𝔸 ∩ ℝ)))
211	110, 209, 210	mp2 9	. . . . . . . . . . . 12 ⊢ ℚ ⊊ (𝔸 ∩ ℝ)
212		psseq1 4037	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ℚ → (𝑥 ⊊ 𝑦 ↔ ℚ ⊊ 𝑦))
213		psseq2 4038	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝔸 ∩ ℝ) → (ℚ ⊊ 𝑦 ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
214	212, 213, 43	brabg 5477	. . . . . . . . . . . . 13 ⊢ ((ℚ ∈ V ∧ (𝔸 ∩ ℝ) ∈ V) → (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ)))
215	11, 8, 214	mp2an 692	. . . . . . . . . . . 12 ⊢ (ℚ < (𝔸 ∩ ℝ) ↔ ℚ ⊊ (𝔸 ∩ ℝ))
216	211, 215	mpbir 231	. . . . . . . . . . 11 ⊢ ℚ < (𝔸 ∩ ℝ)
217	107, 216	eqbrtri 5110	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)
218	217	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ))
219	218	olcd 874	. . . . . . . 8 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ”⟩) < (𝔸 ∩ ℝ)))
220	9, 93, 219	chnccats1 18531	. . . . . . 7 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ”⟩ ++ ⟨“(𝔸 ∩ ℝ)”⟩) ∈ ( < Chain V))
221	7, 220	eqeltrid 2835	. . . . . 6 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ ( < Chain V))
222		s6cli 14791	. . . . . . . . . . . 12 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ∈ Word V
223		lsw 14471	. . . . . . . . . . . 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 14808	. . . . . . . . . . . . . 14 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = 6
226	225	oveq1i 7356	. . . . . . . . . . . . 13 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = (6 − 1)
227		6m1e5 12251	. . . . . . . . . . . . 13 ⊢ (6 − 1) = 5
228	226, 227	eqtri 2754	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1) = 5
229	228	fveq2i 6825	. . . . . . . . . . 11 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
230	224, 229	eqtri 2754	. . . . . . . . . 10 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5)
231	7, 94, 97	cats1fvn 14765	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ))
232	8, 231	ax-mp 5	. . . . . . . . . 10 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩‘5) = (𝔸 ∩ ℝ)
233	230, 232	eqtri 2754	. . . . . . . . 9 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) = (𝔸 ∩ ℝ)
234		inss2 4185	. . . . . . . . . . 11 ⊢ (𝔸 ∩ ℝ) ⊆ ℝ
235		nnuz 12775	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ≥‘1)
236		1zzd 12503	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℤ)
237		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
238		ovexd 7381	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ V)
239		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑘 → 𝑎 = 𝑘)
240	239	fveq2d 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑘 → (!‘𝑎) = (!‘𝑘))
241	240	negeqd 11354	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑘 → -(!‘𝑎) = -(!‘𝑘))
242	241	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑘 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑘)))
243		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
244	242, 243	fvmptg 6927	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ (2↑-(!‘𝑘)) ∈ V) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
245	237, 238, 244	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
246	245	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑘) = (2↑-(!‘𝑘)))
247	157	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
248		2ne0 12229	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
249	248	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → 2 ≠ 0)
250		nnnn0 12388	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
251	250	faccld 14191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (!‘𝑘) ∈ ℕ)
252		nnz 12489	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℕ → (!‘𝑘) ∈ ℤ)
253		znegcl 12507	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) ∈ ℤ → -(!‘𝑘) ∈ ℤ)
254	251, 252, 253	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → -(!‘𝑘) ∈ ℤ)
255	247, 249, 254	reexpclzd 14156	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (2↑-(!‘𝑘)) ∈ ℝ)
256	255	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (2↑-(!‘𝑘)) ∈ ℝ)
257		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1)))) = (𝑛 ∈ (ℤ≥‘1) ↦ ((2↑-(!‘1)) · ((1 / 2)↑(𝑛 − 1))))
258	257, 243	aaliou3lem3 26279	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ → (seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘1)((𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))‘𝑏) ≤ (2 · (2↑-(!‘1)))))
259	258	simp1d 1142	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℕ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
260	27, 259	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (⊤ → seq1( + , (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))) ∈ dom ⇝ )
261	235, 236, 246, 256, 260	isumrecl 15672	. . . . . . . . . . . . 13 ⊢ (⊤ → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ)
262	261	mptru 1548	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ
263		aaliou3 26286	. . . . . . . . . . . . . 14 ⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸
264		df-nel 3033	. . . . . . . . . . . . . 14 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸 ↔ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
265	263, 264	mpbi 230	. . . . . . . . . . . . 13 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸
266		elinel1 4148	. . . . . . . . . . . . 13 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ) → Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ 𝔸)
267	265, 266	mto 197	. . . . . . . . . . . 12 ⊢ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)
268	262, 267	pm3.2i 470	. . . . . . . . . . 11 ⊢ (Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ))
269		ssnelpss 4061	. . . . . . . . . . 11 ⊢ ((𝔸 ∩ ℝ) ⊆ ℝ → ((Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ ∧ ¬ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ (𝔸 ∩ ℝ)) → (𝔸 ∩ ℝ) ⊊ ℝ))
270	234, 268, 269	mp2 9	. . . . . . . . . 10 ⊢ (𝔸 ∩ ℝ) ⊊ ℝ
271		psseq1 4037	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝔸 ∩ ℝ) → (𝑥 ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ 𝑦))
272		psseq2 4038	. . . . . . . . . . . 12 ⊢ (𝑦 = ℝ → ((𝔸 ∩ ℝ) ⊊ 𝑦 ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
273	271, 272, 43	brabg 5477	. . . . . . . . . . 11 ⊢ (((𝔸 ∩ ℝ) ∈ V ∧ ℝ ∈ V) → ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ))
274	8, 5, 273	mp2an 692	. . . . . . . . . 10 ⊢ ((𝔸 ∩ ℝ) < ℝ ↔ (𝔸 ∩ ℝ) ⊊ ℝ)
275	270, 274	mpbir 231	. . . . . . . . 9 ⊢ (𝔸 ∩ ℝ) < ℝ
276	233, 275	eqbrtri 5110	. . . . . . . 8 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ
277	276	a1i 11	. . . . . . 7 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ)
278	277	olcd 874	. . . . . 6 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩) < ℝ))
279	6, 221, 278	chnccats1 18531	. . . . 5 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)”⟩ ++ ⟨“ℝ”⟩) ∈ ( < Chain V))
280	4, 279	eqeltrid 2835	. . . 4 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ ( < Chain V))
281		s7cli 14792	. . . . . . . . 9 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ∈ Word V
282		lsw 14471	. . . . . . . . 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 14809	. . . . . . . . . . . 12 ⊢ (♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = 7
285	284	oveq1i 7356	. . . . . . . . . . 11 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = (7 − 1)
286		7m1e6 12252	. . . . . . . . . . 11 ⊢ (7 − 1) = 6
287	285, 286	eqtri 2754	. . . . . . . . . 10 ⊢ ((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1) = 6
288	287	fveq2i 6825	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6)
289	4, 222, 225	cats1fvn 14765	. . . . . . . . . 10 ⊢ (ℝ ∈ V → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ)
290	5, 289	ax-mp 5	. . . . . . . . 9 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘6) = ℝ
291	288, 290	eqtri 2754	. . . . . . . 8 ⊢ (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩‘((♯‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) − 1)) = ℝ
292	283, 291	eqtri 2754	. . . . . . 7 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) = ℝ
293	81	simpri 485	. . . . . . . . 9 ⊢ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ)
294	293	simpri 485	. . . . . . . 8 ⊢ ℝ ⊊ ℂ
295		psseq1 4037	. . . . . . . . . 10 ⊢ (𝑥 = ℝ → (𝑥 ⊊ 𝑦 ↔ ℝ ⊊ 𝑦))
296		psseq2 4038	. . . . . . . . . 10 ⊢ (𝑦 = ℂ → (ℝ ⊊ 𝑦 ↔ ℝ ⊊ ℂ))
297	295, 296, 43	brabg 5477	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ ℂ ∈ V) → (ℝ < ℂ ↔ ℝ ⊊ ℂ))
298	5, 2, 297	mp2an 692	. . . . . . . 8 ⊢ (ℝ < ℂ ↔ ℝ ⊊ ℂ)
299	294, 298	mpbir 231	. . . . . . 7 ⊢ ℝ < ℂ
300	292, 299	eqbrtri 5110	. . . . . 6 ⊢ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ
301	300	a1i 11	. . . . 5 ⊢ (⊤ → (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ)
302	301	olcd 874	. . . 4 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ = ∅ ∨ (lastS‘⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩) < ℂ))
303	3, 280, 302	chnccats1 18531	. . 3 ⊢ (⊤ → (⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝ”⟩ ++ ⟨“ℂ”⟩) ∈ ( < Chain V))
304	1, 303	eqeltrid 2835	. 2 ⊢ (⊤ → ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V))
305	304	mptru 1548	1 ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111   ≠ wne 2928   ∉ wnel 3032  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ∖ cdif 3894   ∩ cin 3896   ⊆ wss 3897   ⊊ wpss 3898  ∅c0 4280  {csn 4573   class class class wbr 5089  {copab 5151   ↦ cmpt 5170   × cxp 5612  dom cdm 5614   Fn wfn 6476  ‘cfv 6481  (class class class)co 7346   ∘_f cof 7608  ℂcc 11004  ℝcr 11005  0cc0 11006  1c1 11007   + caddc 11009   · cmul 11011   < clt 11146   ≤ cle 11147   − cmin 11344  -cneg 11345   / cdiv 11774  ℕcn 12125  2c2 12180  4c4 12182  5c5 12183  6c6 12184  7c7 12185  ℕ₀cn0 12381  ℤcz 12468  ℤ_≥cuz 12732  ℚcq 12846  ℝ⁺crp 12890  seqcseq 13908  ↑cexp 13968  !cfa 14180  ♯chash 14237  Word cword 14420  lastSclsw 14469   ++ cconcat 14477  ⟨“cs1 14503  ⟨“cs2 14748  ⟨“cs3 14749  ⟨“cs4 14750  ⟨“cs5 14751  ⟨“cs6 14752  ⟨“cs7 14753  ⟨“cs8 14754  √csqrt 15140   ⇝ cli 15391  Σcsu 15593   Chain cchn 18511  0_𝑝c0p 25597  Polycply 26116  𝔸caa 26249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-inf2 9531  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084  ax-addf 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4857  df-int 4896  df-iun 4941  df-iin 4942  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7610  df-om 7797  df-1st 7921  df-2nd 7922  df-supp 8091  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-oadd 8389  df-er 8622  df-map 8752  df-pm 8753  df-ixp 8822  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-fsupp 9246  df-fi 9295  df-sup 9326  df-inf 9327  df-oi 9396  df-dju 9794  df-card 9832  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194  df-9 12195  df-n0 12382  df-xnn0 12455  df-z 12469  df-dec 12589  df-uz 12733  df-q 12847  df-rp 12891  df-xneg 13011  df-xadd 13012  df-xmul 13013  df-ioo 13249  df-ioc 13250  df-ico 13251  df-icc 13252  df-fz 13408  df-fzo 13555  df-fl 13696  df-mod 13774  df-seq 13909  df-exp 13969  df-fac 14181  df-hash 14238  df-word 14421  df-lsw 14470  df-concat 14478  df-s1 14504  df-s2 14755  df-s3 14756  df-s4 14757  df-s5 14758  df-s6 14759  df-s7 14760  df-s8 14761  df-shft 14974  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-limsup 15378  df-clim 15395  df-rlim 15396  df-sum 15594  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-starv 17176  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-unif 17184  df-hom 17185  df-cco 17186  df-rest 17326  df-topn 17327  df-0g 17345  df-gsum 17346  df-topgen 17347  df-pt 17348  df-prds 17351  df-xrs 17406  df-qtop 17411  df-imas 17412  df-xps 17414  df-mre 17488  df-mrc 17489  df-acs 17491  df-chn 18512  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-submnd 18692  df-grp 18849  df-minusg 18850  df-mulg 18981  df-subg 19036  df-cntz 19229  df-cmn 19694  df-abl 19695  df-mgp 20059  df-rng 20071  df-ur 20100  df-ring 20153  df-cring 20154  df-subrng 20461  df-subrg 20485  df-psmet 21283  df-xmet 21284  df-met 21285  df-bl 21286  df-mopn 21287  df-fbas 21288  df-fg 21289  df-cnfld 21292  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22861  df-cld 22934  df-ntr 22935  df-cls 22936  df-nei 23013  df-lp 23051  df-perf 23052  df-cn 23142  df-cnp 23143  df-haus 23230  df-cmp 23302  df-tx 23477  df-hmeo 23670  df-fil 23761  df-fm 23853  df-flim 23854  df-flf 23855  df-xms 24235  df-ms 24236  df-tms 24237  df-cncf 24798  df-0p 25598  df-limc 25794  df-dv 25795  df-dvn 25796  df-cpn 25797  df-ply 26120  df-idp 26121  df-coe 26122  df-dgr 26123  df-quot 26226  df-aa 26250

This theorem is referenced by: (None)