rrhre - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrhre		Structured version Visualization version GIF version

Theorem rrhre 34004

Description: The ℝHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017.)

**Assertion**
Ref	Expression
rrhre	⊢ (ℝHom‘ℝ_fld) = ( I ↾ ℝ)

Proof of Theorem rrhre Dummy variables 𝑎 𝑏 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniretop 24683	. . 3 ⊢ ℝ = ∪ (topGen‘ran (,))
2		rehaus 24720	. . . 4 ⊢ (topGen‘ran (,)) ∈ Haus
3	2	a1i 11	. . 3 ⊢ (⊤ → (topGen‘ran (,)) ∈ Haus)
4		rerrext 33992	. . . 4 ⊢ ℝ_fld ∈ ℝExt
5		eqid 2729	. . . . 5 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
6		retopn 25312	. . . . 5 ⊢ (topGen‘ran (,)) = (TopOpen‘ℝ_fld)
7	5, 6	rrhcne 33996	. . . 4 ⊢ (ℝ_fld ∈ ℝExt → (ℝHom‘ℝ_fld) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
8	4, 7	mp1i 13	. . 3 ⊢ (⊤ → (ℝHom‘ℝ_fld) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
9		retop 24682	. . . . . 6 ⊢ (topGen‘ran (,)) ∈ Top
10	1	toptopon 22837	. . . . . 6 ⊢ ((topGen‘ran (,)) ∈ Top ↔ (topGen‘ran (,)) ∈ (TopOn‘ℝ))
11	9, 10	mpbi 230	. . . . 5 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
12		idcn 23177	. . . . 5 ⊢ ((topGen‘ran (,)) ∈ (TopOn‘ℝ) → ( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
13	11, 12	ax-mp 5	. . . 4 ⊢ ( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,)))
14	13	a1i 11	. . 3 ⊢ (⊤ → ( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
15	9	a1i 11	. . . . . . 7 ⊢ (⊤ → (topGen‘ran (,)) ∈ Top)
16		f1oi 6820	. . . . . . . . . 10 ⊢ ( I ↾ ℚ):ℚ–1-1-onto→ℚ
17		f1of 6782	. . . . . . . . . 10 ⊢ (( I ↾ ℚ):ℚ–1-1-onto→ℚ → ( I ↾ ℚ):ℚ⟶ℚ)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ( I ↾ ℚ):ℚ⟶ℚ
19		qssre 12894	. . . . . . . . 9 ⊢ ℚ ⊆ ℝ
20		fss 6686	. . . . . . . . 9 ⊢ ((( I ↾ ℚ):ℚ⟶ℚ ∧ ℚ ⊆ ℝ) → ( I ↾ ℚ):ℚ⟶ℝ)
21	18, 19, 20	mp2an 692	. . . . . . . 8 ⊢ ( I ↾ ℚ):ℚ⟶ℝ
22	21	a1i 11	. . . . . . 7 ⊢ (⊤ → ( I ↾ ℚ):ℚ⟶ℝ)
23	19	a1i 11	. . . . . . 7 ⊢ (⊤ → ℚ ⊆ ℝ)
24		qdensere 24690	. . . . . . . 8 ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
25	24	a1i 11	. . . . . . 7 ⊢ (⊤ → ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ)
26	9	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (topGen‘ran (,)) ∈ Top)
27		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ (topGen‘ran (,)))
28		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎)
29		opnneip 23039	. . . . . . . . . . . . . . . 16 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑎 ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}))
30	26, 27, 28, 29	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}))
31		fvex 6853	. . . . . . . . . . . . . . . 16 ⊢ ((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V
32		qex 12896	. . . . . . . . . . . . . . . 16 ⊢ ℚ ∈ V
33		elrestr 17367	. . . . . . . . . . . . . . . 16 ⊢ ((((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V ∧ ℚ ∈ V ∧ 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥})) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
34	31, 32, 33	mp3an12 1453	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
35	30, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
36		inss2 4197	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∩ ℚ) ⊆ ℚ
37		resiima 6036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∩ ℚ) ⊆ ℚ → (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) = (𝑎 ∩ ℚ))
38	36, 37	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) = (𝑎 ∩ ℚ)
39		inss1 4196	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∩ ℚ) ⊆ 𝑎
40	38, 39	eqsstri 3990	. . . . . . . . . . . . . . 15 ⊢ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎
41	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎)
42		imaeq2 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑎 ∩ ℚ) → (( I ↾ ℚ) “ 𝑏) = (( I ↾ ℚ) “ (𝑎 ∩ ℚ)))
43	42	sseq1d 3975	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑎 ∩ ℚ) → ((( I ↾ ℚ) “ 𝑏) ⊆ 𝑎 ↔ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎))
44	43	rspcev 3585	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∧ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎) → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)
45	35, 41, 44	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)
46	45	ex 412	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) → (𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))
47	46	ralrimiva 3125	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))
48	47	ancli 548	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)))
49	24	eleq2i 2820	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ 𝑥 ∈ ℝ)
50	49	biimpri 228	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ))
51		trnei 23812	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ℚ ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ)))
52	11, 19, 51	mp3an12 1453	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ)))
53	50, 52	mpbid 232	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ))
54		isflf 23913	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ) ∧ ( I ↾ ℚ):ℚ⟶ℝ) → (𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ↔ (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))))
55	11, 21, 54	mp3an13 1454	. . . . . . . . . . 11 ⊢ ((((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ) → (𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ↔ (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))))
56	53, 55	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ↔ (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))))
57	48, 56	mpbird 257	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)))
58	57	ne0d 4301	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ≠ ∅)
59	58	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ≠ ∅)
60		recusp 25315	. . . . . . . . . 10 ⊢ ℝ_fld ∈ CUnifSp
61		cuspusp 24220	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ CUnifSp → ℝ_fld ∈ UnifSp)
62	60, 61	ax-mp 5	. . . . . . . . 9 ⊢ ℝ_fld ∈ UnifSp
63	6	uspreg 24194	. . . . . . . . 9 ⊢ ((ℝ_fld ∈ UnifSp ∧ (topGen‘ran (,)) ∈ Haus) → (topGen‘ran (,)) ∈ Reg)
64	62, 2, 63	mp2an 692	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Reg
65	64	a1i 11	. . . . . . 7 ⊢ (⊤ → (topGen‘ran (,)) ∈ Reg)
66		resabs1 5966	. . . . . . . . . 10 ⊢ (ℚ ⊆ ℝ → (( I ↾ ℝ) ↾ ℚ) = ( I ↾ ℚ))
67	19, 66	ax-mp 5	. . . . . . . . 9 ⊢ (( I ↾ ℝ) ↾ ℚ) = ( I ↾ ℚ)
68	1	cnrest 23205	. . . . . . . . . 10 ⊢ ((( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))) ∧ ℚ ⊆ ℝ) → (( I ↾ ℝ) ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,))))
69	13, 19, 68	mp2an 692	. . . . . . . . 9 ⊢ (( I ↾ ℝ) ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,)))
70	67, 69	eqeltrri 2825	. . . . . . . 8 ⊢ ( I ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,)))
71	70	a1i 11	. . . . . . 7 ⊢ (⊤ → ( I ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,))))
72	1, 1, 15, 3, 22, 23, 25, 59, 65, 71	cnextfres1 23988	. . . . . 6 ⊢ (⊤ → ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ) = ( I ↾ ℚ))
73	72	mptru 1547	. . . . 5 ⊢ ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ) = ( I ↾ ℚ)
74		recms 25313	. . . . . . . . 9 ⊢ ℝ_fld ∈ CMetSp
75	74	elexi 3467	. . . . . . . 8 ⊢ ℝ_fld ∈ V
76	5, 6	rrhval 33979	. . . . . . . 8 ⊢ (ℝ_fld ∈ V → (ℝHom‘ℝ_fld) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘(ℚHom‘ℝ_fld)))
77	75, 76	ax-mp 5	. . . . . . 7 ⊢ (ℝHom‘ℝ_fld) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘(ℚHom‘ℝ_fld))
78		qqhre 34003	. . . . . . . 8 ⊢ (ℚHom‘ℝ_fld) = ( I ↾ ℚ)
79	78	fveq2i 6843	. . . . . . 7 ⊢ (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘(ℚHom‘ℝ_fld)) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ))
80	77, 79	eqtri 2752	. . . . . 6 ⊢ (ℝHom‘ℝ_fld) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ))
81	80	reseq1i 5935	. . . . 5 ⊢ ((ℝHom‘ℝ_fld) ↾ ℚ) = ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ)
82	73, 81, 67	3eqtr4i 2762	. . . 4 ⊢ ((ℝHom‘ℝ_fld) ↾ ℚ) = (( I ↾ ℝ) ↾ ℚ)
83	82	a1i 11	. . 3 ⊢ (⊤ → ((ℝHom‘ℝ_fld) ↾ ℚ) = (( I ↾ ℝ) ↾ ℚ))
84	1, 3, 8, 14, 83, 23, 25	hauseqcn 33881	. 2 ⊢ (⊤ → (ℝHom‘ℝ_fld) = ( I ↾ ℝ))
85	84	mptru 1547	1 ⊢ (ℝHom‘ℝ_fld) = ( I ↾ ℝ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 {csn 4585 I cid 5525 ran crn 5632 ↾ cres 5633 “ cima 5634 ⟶wf 6495 –1-1-onto→wf1o 6498 ‘cfv 6499 (class class class)co 7369 ℝcr 11043 ℚcq 12883 (,)cioo 13282 ↾_t crest 17359 topGenctg 17376 ℝ_fldcrefld 21546 Topctop 22813 TopOnctopon 22830 clsccl 22938 neicnei 23017 Cn ccn 23144 Hauscha 23228 Regcreg 23229 Filcfil 23765 fLimf cflf 23855 CnExtccnext 23979 UnifSpcusp 24175 CUnifSpccusp 24217 CMetSpccms 25265 ℚHomcqqh 33953 ℝHomcrrh 33976 ℝExt crrext 33977

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123 ax-mulf 11124

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-tpos 8182 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-fi 9338 df-sup 9369 df-inf 9370 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-fl 13730 df-mod 13808 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-dvds 16199 df-gcd 16441 df-numer 16681 df-denom 16682 df-gz 16877 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17361 df-topn 17362 df-0g 17380 df-gsum 17381 df-topgen 17382 df-pt 17383 df-prds 17386 df-xrs 17441 df-qtop 17446 df-imas 17447 df-xps 17449 df-mre 17523 df-mrc 17524 df-acs 17526 df-proset 18235 df-poset 18254 df-plt 18269 df-toset 18356 df-ps 18507 df-tsr 18508 df-mgm 18549 df-sgrp 18628 df-mnd 18644 df-mhm 18692 df-submnd 18693 df-grp 18850 df-minusg 18851 df-sbg 18852 df-mulg 18982 df-subg 19037 df-ghm 19127 df-cntz 19231 df-od 19442 df-cmn 19696 df-abl 19697 df-omnd 20035 df-ogrp 20036 df-mgp 20061 df-rng 20073 df-ur 20102 df-ring 20155 df-cring 20156 df-oppr 20257 df-dvdsr 20277 df-unit 20278 df-invr 20308 df-dvr 20321 df-rhm 20392 df-nzr 20433 df-subrng 20466 df-subrg 20490 df-drng 20651 df-field 20652 df-abv 20729 df-orng 20779 df-ofld 20780 df-lmod 20800 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-fbas 21293 df-fg 21294 df-metu 21295 df-cnfld 21297 df-zring 21389 df-zrh 21445 df-zlm 21446 df-chr 21447 df-refld 21547 df-top 22814 df-topon 22831 df-topsp 22853 df-bases 22866 df-cld 22939 df-ntr 22940 df-cls 22941 df-nei 23018 df-cn 23147 df-cnp 23148 df-haus 23235 df-reg 23236 df-cmp 23307 df-tx 23482 df-hmeo 23675 df-fil 23766 df-fm 23858 df-flim 23859 df-flf 23860 df-fcls 23861 df-cnext 23980 df-ust 24121 df-utop 24152 df-uss 24177 df-usp 24178 df-ucn 24196 df-cfilu 24207 df-cusp 24218 df-xms 24241 df-ms 24242 df-tms 24243 df-nm 24503 df-ngp 24504 df-nrg 24506 df-nlm 24507 df-cncf 24804 df-cfil 25188 df-cmet 25190 df-cms 25268 df-qqh 33954 df-rrh 33978 df-rrext 33982

This theorem is referenced by: sitmcl 34335

W3C validator