Theorem constrextdg2 34424

Description: Any step (𝐶‘𝑁) of the construction of constructible numbers is contained in the last field of a tower of quadratic field extensions starting with ℚ. See Theorem 7.11 of [Stewart] p. 97. (Contributed by Thierry Arnoux, 19-Oct-2025.)

Hypotheses

Ref	Expression
constr0.1	⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
constrextdg2.1	⊢ 𝐸 = (ℂfld ↾s 𝑒)
constrextdg2.2	⊢ 𝐹 = (ℂfld ↾s 𝑓)
constrextdg2.l	⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
constrextdg2.n	⊢ (𝜑 → 𝑁 ∈ ω)

Assertion

Ref	Expression
constrextdg2	⊢ (𝜑 → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣)))

Distinct variable groups:   < ,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑟,𝑠,𝑡,𝑣,𝑥   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑟,𝑠,𝑡,𝑣,𝑥   𝑡,𝑁,𝑣

Allowed substitution hints:   𝜑(𝑥, 𝑣, 𝑡, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)   𝐸(𝑥, 𝑣, 𝑡, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)   𝐹(𝑥, 𝑣, 𝑡, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)   𝑁(𝑥, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem constrextdg2

Dummy variables 𝑛 𝑢 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		constrextdg2.n	. 2 ⊢ (𝜑 → 𝑁 ∈ ω)
2		fveq2 6885	. . . . . 6 ⊢ (𝑚 = ∅ → (𝐶‘𝑚) = (𝐶‘∅))
3	2	sseq1d 3939	. . . . 5 ⊢ (𝑚 = ∅ → ((𝐶‘𝑚) ⊆ (lastS‘𝑣) ↔ (𝐶‘∅) ⊆ (lastS‘𝑣)))
4	3	anbi2d 642	. . . 4 ⊢ (𝑚 = ∅ → (((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ((𝑣‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘𝑣))))
5	4	rexbidv 3186	. . 3 ⊢ (𝑚 = ∅ → (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘𝑣))))
6		fveq2 6885	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛))
7	6	sseq1d 3939	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚) ⊆ (lastS‘𝑣) ↔ (𝐶‘𝑛) ⊆ (lastS‘𝑣)))
8	7	anbi2d 642	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ((𝑣‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑣))))
9	8	rexbidv 3186	. . . 4 ⊢ (𝑚 = 𝑛 → (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑣))))
10		fveq1 6884	. . . . . . 7 ⊢ (𝑣 = 𝑢 → (𝑣‘0) = (𝑢‘0))
11	10	eqeq1d 2762	. . . . . 6 ⊢ (𝑣 = 𝑢 → ((𝑣‘0) = ℚ ↔ (𝑢‘0) = ℚ))
12		fveq2 6885	. . . . . . 7 ⊢ (𝑣 = 𝑢 → (lastS‘𝑣) = (lastS‘𝑢))
13	12	sseq2d 3940	. . . . . 6 ⊢ (𝑣 = 𝑢 → ((𝐶‘𝑛) ⊆ (lastS‘𝑣) ↔ (𝐶‘𝑛) ⊆ (lastS‘𝑢)))
14	11, 13	anbi12d 644	. . . . 5 ⊢ (𝑣 = 𝑢 → (((𝑣‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑣)) ↔ ((𝑢‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢))))
15	14	cbvrexvw 3241	. . . 4 ⊢ (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑣)) ↔ ∃𝑢 ∈ ( < Chain (SubDRing‘ℂfld))((𝑢‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)))
16	9, 15	bitrdi 290	. . 3 ⊢ (𝑚 = 𝑛 → (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ∃𝑢 ∈ ( < Chain (SubDRing‘ℂfld))((𝑢‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢))))
17		fveq2 6885	. . . . . 6 ⊢ (𝑚 = suc 𝑛 → (𝐶‘𝑚) = (𝐶‘suc 𝑛))
18	17	sseq1d 3939	. . . . 5 ⊢ (𝑚 = suc 𝑛 → ((𝐶‘𝑚) ⊆ (lastS‘𝑣) ↔ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣)))
19	18	anbi2d 642	. . . 4 ⊢ (𝑚 = suc 𝑛 → (((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣))))
20	19	rexbidv 3186	. . 3 ⊢ (𝑚 = suc 𝑛 → (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣))))
21		fveq2 6885	. . . . . 6 ⊢ (𝑚 = 𝑁 → (𝐶‘𝑚) = (𝐶‘𝑁))
22	21	sseq1d 3939	. . . . 5 ⊢ (𝑚 = 𝑁 → ((𝐶‘𝑚) ⊆ (lastS‘𝑣) ↔ (𝐶‘𝑁) ⊆ (lastS‘𝑣)))
23	22	anbi2d 642	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣))))
24	23	rexbidv 3186	. . 3 ⊢ (𝑚 = 𝑁 → (∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑚) ⊆ (lastS‘𝑣)) ↔ ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣))))
25		fveq1 6884	. . . . . . 7 ⊢ (𝑣 = ⟨“ℚ”⟩ → (𝑣‘0) = (⟨“ℚ”⟩‘0))
26	25	eqeq1d 2762	. . . . . 6 ⊢ (𝑣 = ⟨“ℚ”⟩ → ((𝑣‘0) = ℚ ↔ (⟨“ℚ”⟩‘0) = ℚ))
27		fveq2 6885	. . . . . . 7 ⊢ (𝑣 = ⟨“ℚ”⟩ → (lastS‘𝑣) = (lastS‘⟨“ℚ”⟩))
28	27	sseq2d 3940	. . . . . 6 ⊢ (𝑣 = ⟨“ℚ”⟩ → ((𝐶‘∅) ⊆ (lastS‘𝑣) ↔ (𝐶‘∅) ⊆ (lastS‘⟨“ℚ”⟩)))
29	26, 28	anbi12d 644	. . . . 5 ⊢ (𝑣 = ⟨“ℚ”⟩ → (((𝑣‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘𝑣)) ↔ ((⟨“ℚ”⟩‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘⟨“ℚ”⟩))))
30		cndrng 21708	. . . . . . . 8 ⊢ ℂfld ∈ DivRing
31		qsubdrg 21726	. . . . . . . . 9 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
32	31	simpli 489	. . . . . . . 8 ⊢ ℚ ∈ (SubRing‘ℂfld)
33	31	simpri 491	. . . . . . . 8 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
34		issdrg 21046	. . . . . . . 8 ⊢ (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing))
35	30, 32, 33, 34	mpbir3an 1360	. . . . . . 7 ⊢ ℚ ∈ (SubDRing‘ℂfld)
36	35	a1i 11	. . . . . 6 ⊢ (⊤ → ℚ ∈ (SubDRing‘ℂfld))
37	36	s1chn 18795	. . . . 5 ⊢ (⊤ → ⟨“ℚ”⟩ ∈ ( < Chain (SubDRing‘ℂfld)))
38		s1fv 14759	. . . . . . 7 ⊢ (ℚ ∈ (SubDRing‘ℂfld) → (⟨“ℚ”⟩‘0) = ℚ)
39	36, 38	syl 18	. . . . . 6 ⊢ (⊤ → (⟨“ℚ”⟩‘0) = ℚ)
40		0z 12705	. . . . . . . . 9 ⊢ 0 ∈ ℤ
41		1z 12727	. . . . . . . . 9 ⊢ 1 ∈ ℤ
42		prssi 4781	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → {0, 1} ⊆ ℤ)
43	40, 41, 42	mp2an 705	. . . . . . . 8 ⊢ {0, 1} ⊆ ℤ
44		zssq 13084	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
45	43, 44	sstri 3917	. . . . . . 7 ⊢ {0, 1} ⊆ ℚ
46		constr0.1	. . . . . . . 8 ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
47	46	constr0 34412	. . . . . . 7 ⊢ (𝐶‘∅) = {0, 1}
48		lsws1 14760	. . . . . . . 8 ⊢ (ℚ ∈ (SubDRing‘ℂfld) → (lastS‘⟨“ℚ”⟩) = ℚ)
49	35, 48	ax-mp 5	. . . . . . 7 ⊢ (lastS‘⟨“ℚ”⟩) = ℚ
50	45, 47, 49	3sstr4i 3959	. . . . . 6 ⊢ (𝐶‘∅) ⊆ (lastS‘⟨“ℚ”⟩)
51	39, 50	jctir 530	. . . . 5 ⊢ (⊤ → ((⟨“ℚ”⟩‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘⟨“ℚ”⟩)))
52	29, 37, 51	rspcedvdw 3579	. . . 4 ⊢ (⊤ → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘𝑣)))
53	52	mptru 1576	. . 3 ⊢ ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘∅) ⊆ (lastS‘𝑣))
54		constrextdg2.1	. . . . . 6 ⊢ 𝐸 = (ℂfld ↾s 𝑒)
55		constrextdg2.2	. . . . . 6 ⊢ 𝐹 = (ℂfld ↾s 𝑓)
56		constrextdg2.l	. . . . . 6 ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
57		simplll 787	. . . . . 6 ⊢ ((((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ (𝑢‘0) = ℚ) ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → 𝑛 ∈ ω)
58		simpllr 788	. . . . . 6 ⊢ ((((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ (𝑢‘0) = ℚ) ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → 𝑢 ∈ ( < Chain (SubDRing‘ℂfld)))
59		simplr 781	. . . . . 6 ⊢ ((((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ (𝑢‘0) = ℚ) ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → (𝑢‘0) = ℚ)
60		simpr 490	. . . . . 6 ⊢ ((((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ (𝑢‘0) = ℚ) ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → (𝐶‘𝑛) ⊆ (lastS‘𝑢))
61	46, 54, 55, 56, 57, 58, 59, 60	constrextdg2lem 34423	. . . . 5 ⊢ ((((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ (𝑢‘0) = ℚ) ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣)))
62	61	anasss 472	. . . 4 ⊢ (((𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain (SubDRing‘ℂfld))) ∧ ((𝑢‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢))) → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣)))
63	62	rexlimdva2 3165	. . 3 ⊢ (𝑛 ∈ ω → (∃𝑢 ∈ ( < Chain (SubDRing‘ℂfld))((𝑢‘0) = ℚ ∧ (𝐶‘𝑛) ⊆ (lastS‘𝑢)) → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑛) ⊆ (lastS‘𝑣))))
64	5, 16, 20, 24, 53, 63	finds 7908	. 2 ⊢ (𝑁 ∈ ω → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣)))
65	1, 64	syl 18	1 ⊢ (𝜑 → ∃𝑣 ∈ ( < Chain (SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  {cpr 4585   class class class wbr 5102  {copab 5166   ↦ cmpt 5185  suc csuc 6364  ‘cfv 6538  (class class class)co 7420  ωcom 7877  reccrdg 8418  ℂcc 11199  ℝcr 11200  0cc0 11201  1c1 11202   + caddc 11204   · cmul 11206   − cmin 11542  2c2 12398  ℤcz 12694  ℚcq 13076  lastSclsw 14708  ⟨“cs1 14743  ∗ccj 15264  ℑcim 15266  abscabs 15402   ↾_s cress 17409   Chain cchn 18780  SubRingcsubrg 20822  DivRingcdr 20981  SubDRingcsdrg 21044  ℂ_fldccnfld 21679  /_FldExtcfldext 34313  [:]cextdg 34315

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-reg 9587  ax-inf2 9643  ax-ac2 10542  ax-cnex 11257  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277  ax-pre-mulgt0 11278  ax-pre-sup 11279  ax-addf 11280  ax-mulf 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-ofr 7694  df-rpss 7739  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8178  df-tpos 8244  df-frecs 8300  df-wrecs 8331  df-recs 8380  df-rdg 8419  df-1o 8477  df-2o 8478  df-oadd 8481  df-er 8718  df-ec 8720  df-qs 8724  df-map 8850  df-pm 8851  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9355  df-sup 9435  df-inf 9436  df-oi 9505  df-r1 9769  df-rank 9770  df-scott 9930  df-dju 9983  df-card 10021  df-acn 10024  df-ac 10196  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-sub 11544  df-neg 11545  df-div 11975  df-nn 12337  df-2 12406  df-3 12407  df-4 12408  df-5 12409  df-6 12410  df-7 12411  df-8 12412  df-9 12413  df-n0 12608  df-xnn0 12681  df-z 12695  df-dec 12816  df-uz 12967  df-q 13077  df-rp 13122  df-ico 13483  df-fz 13641  df-fzo 13790  df-seq 14146  df-exp 14206  df-hash 14476  df-word 14660  df-lsw 14709  df-concat 14717  df-s1 14744  df-cj 15267  df-re 15268  df-im 15269  df-sqrt 15403  df-abs 15404  df-struct 17326  df-sets 17343  df-slot 17361  df-ndx 17373  df-base 17389  df-ress 17410  df-plusg 17442  df-mulr 17443  df-starv 17444  df-sca 17445  df-vsca 17446  df-ip 17447  df-tset 17448  df-ple 17449  df-ocomp 17450  df-ds 17451  df-unif 17452  df-hom 17453  df-cco 17454  df-0g 17613  df-gsum 17614  df-prds 17619  df-pws 17621  df-imas 17681  df-qus 17682  df-mre 17757  df-mrc 17758  df-mri 17759  df-acs 17760  df-proset 18469  df-drs 18470  df-poset 18488  df-ipo 18703  df-chn 18781  df-mgm 18817  df-sgrp 18909  df-mnd 18925  df-mhm 18979  df-submnd 18980  df-grp 19148  df-minusg 19149  df-sbg 19150  df-mulg 19279  df-subg 19334  df-nsg 19335  df-eqg 19336  df-ghm 19429  df-gim 19474  df-cntz 19532  df-oppg 19561  df-lsm 19851  df-cmn 19997  df-abl 19998  df-mgp 20362  df-rng 20376  df-ur 20409  df-srg 20414  df-ring 20462  df-cring 20463  df-oppr 20568  df-dvdsr 20588  df-unit 20589  df-irred 20590  df-invr 20619  df-dvr 20632  df-rhm 20703  df-nzr 20764  df-subrng 20799  df-subrg 20823  df-rlreg 20947  df-domn 20948  df-idom 20949  df-drng 20983  df-field 20984  df-sdrg 21045  df-lmod 21138  df-lss 21208  df-lsp 21248  df-lmhm 21298  df-lmim 21299  df-lmic 21300  df-lbs 21351  df-lvec 21379  df-sra 21449  df-rgmod 21450  df-lidl 21487  df-rsp 21488  df-2idl 21544  df-lpidl 21647  df-lpir 21648  df-pid 21662  df-cnfld 21680  df-dsmm 22039  df-frlm 22054  df-uvc 22090  df-lindf 22113  df-linds 22114  df-assa 22162  df-asp 22163  df-ascl 22164  df-psr 22218  df-mvr 22219  df-mpl 22220  df-opsr 22222  df-evls 22384  df-evl 22385  df-psr1 22499  df-vr1 22500  df-ply1 22501  df-coe1 22502  df-evls1 22634  df-evl1 22635  df-mdeg 26374  df-deg1 26375  df-mon1 26450  df-uc1p 26451  df-q1p 26452  df-r1p 26453  df-ig1p 26454  df-fldgen 33916  df-mxidl 34028  df-dim 34275  df-fldext 34316  df-extdg 34317  df-irng 34359  df-minply 34375

This theorem is used by:  constrext2chnlem  34425