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 34653

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 25081	. . 3 ⊢ ℝ = ∪ (topGen‘ran (,))
2		rehaus 25118	. . . 4 ⊢ (topGen‘ran (,)) ∈ Haus
3	2	a1i 11	. . 3 ⊢ (⊤ → (topGen‘ran (,)) ∈ Haus)
4		rerrext 34641	. . . 4 ⊢ ℝ_fld ∈ ℝExt
5		eqid 2761	. . . . 5 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
6		retopn 25700	. . . . 5 ⊢ (topGen‘ran (,)) = (TopOpen‘ℝ_fld)
7	5, 6	rrhcne 34645	. . . 4 ⊢ (ℝ_fld ∈ ℝExt → (ℝHom‘ℝ_fld) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
8	4, 7	mp1i 14	. . 3 ⊢ (⊤ → (ℝHom‘ℝ_fld) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))))
9		retop 25080	. . . . . 6 ⊢ (topGen‘ran (,)) ∈ Top
10	1	toptopon 23235	. . . . . 6 ⊢ ((topGen‘ran (,)) ∈ Top ↔ (topGen‘ran (,)) ∈ (TopOn‘ℝ))
11	9, 10	mpbi 233	. . . . 5 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
12		idcn 23575	. . . . 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 6863	. . . . . . . . . 10 ⊢ ( I ↾ ℚ):ℚ–1-1-onto→ℚ
17		f1of 6824	. . . . . . . . . 10 ⊢ (( I ↾ ℚ):ℚ–1-1-onto→ℚ → ( I ↾ ℚ):ℚ⟶ℚ)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ( I ↾ ℚ):ℚ⟶ℚ
19		qssre 13086	. . . . . . . . 9 ⊢ ℚ ⊆ ℝ
20		fss 6726	. . . . . . . . 9 ⊢ ((( I ↾ ℚ):ℚ⟶ℚ ∧ ℚ ⊆ ℝ) → ( I ↾ ℚ):ℚ⟶ℝ)
21	18, 19, 20	mp2an 705	. . . . . . . 8 ⊢ ( I ↾ ℚ):ℚ⟶ℝ
22	21	a1i 11	. . . . . . 7 ⊢ (⊤ → ( I ↾ ℚ):ℚ⟶ℝ)
23	19	a1i 11	. . . . . . 7 ⊢ (⊤ → ℚ ⊆ ℝ)
24		qdensere 25088	. . . . . . . 8 ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
25	24	a1i 11	. . . . . . 7 ⊢ (⊤ → ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ)
26	9	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (topGen‘ran (,)) ∈ Top)
27		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ (topGen‘ran (,)))
28		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎)
29		opnneip 23437	. . . . . . . . . . . . . . . 16 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑎 ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}))
30	26, 27, 28, 29	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}))
31		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ ((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V
32		qex 13088	. . . . . . . . . . . . . . . 16 ⊢ ℚ ∈ V
33		elrestr 17599	. . . . . . . . . . . . . . . 16 ⊢ ((((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V ∧ ℚ ∈ V ∧ 𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥})) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
34	31, 32, 33	mp3an12 1480	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((nei‘(topGen‘ran (,)))‘{𝑥}) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
35	30, 34	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))
36		inss2 4183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∩ ℚ) ⊆ ℚ
37		resiima 6074	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∩ ℚ) ⊆ ℚ → (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) = (𝑎 ∩ ℚ))
38	36, 37	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) = (𝑎 ∩ ℚ)
39		inss1 4182	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∩ ℚ) ⊆ 𝑎
40	38, 39	eqsstri 3977	. . . . . . . . . . . . . . 15 ⊢ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎
41	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎)
42		imaeq2 6048	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑎 ∩ ℚ) → (( I ↾ ℚ) “ 𝑏) = (( I ↾ ℚ) “ (𝑎 ∩ ℚ)))
43	42	sseq1d 3962	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑎 ∩ ℚ) → ((( I ↾ ℚ) “ 𝑏) ⊆ 𝑎 ↔ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎))
44	43	rspcev 3577	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∩ ℚ) ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∧ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) ⊆ 𝑎) → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)
45	35, 41, 44	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) ∧ 𝑥 ∈ 𝑎) → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)
46	45	ex 418	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,))) → (𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))
47	46	ralrimiva 3155	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))
48	47	ancli 558	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)))
49	24	eleq2i 2853	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ 𝑥 ∈ ℝ)
50	49	biimpri 231	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ))
51		trnei 24211	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ℚ ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ)))
52	11, 19, 51	mp3an12 1480	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ)))
53	50, 52	mpbid 235	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ) ∈ (Fil‘ℚ))
54		isflf 24312	. . . . . . . . . . . 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 1481	. . . . . . . . . . 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 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ↔ (𝑥 ∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎))))
57	48, 56	mpbird 260	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)))
58	57	ne0d 4288	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ≠ ∅)
59	58	adantl 487	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → (((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾_t ℚ))‘( I ↾ ℚ)) ≠ ∅)
60		recusp 25703	. . . . . . . . . 10 ⊢ ℝ_fld ∈ CUnifSp
61		cuspusp 24618	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ CUnifSp → ℝ_fld ∈ UnifSp)
62	60, 61	ax-mp 5	. . . . . . . . 9 ⊢ ℝ_fld ∈ UnifSp
63	6	uspreg 24592	. . . . . . . . 9 ⊢ ((ℝ_fld ∈ UnifSp ∧ (topGen‘ran (,)) ∈ Haus) → (topGen‘ran (,)) ∈ Reg)
64	62, 2, 63	mp2an 705	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Reg
65	64	a1i 11	. . . . . . 7 ⊢ (⊤ → (topGen‘ran (,)) ∈ Reg)
66		resabs1 5997	. . . . . . . . . 10 ⊢ (ℚ ⊆ ℝ → (( I ↾ ℝ) ↾ ℚ) = ( I ↾ ℚ))
67	19, 66	ax-mp 5	. . . . . . . . 9 ⊢ (( I ↾ ℝ) ↾ ℚ) = ( I ↾ ℚ)
68	1	cnrest 23603	. . . . . . . . . 10 ⊢ ((( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,))) ∧ ℚ ⊆ ℝ) → (( I ↾ ℝ) ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,))))
69	13, 19, 68	mp2an 705	. . . . . . . . 9 ⊢ (( I ↾ ℝ) ↾ ℚ) ∈ (((topGen‘ran (,)) ↾_t ℚ) Cn (topGen‘ran (,)))
70	67, 69	eqeltrri 2858	. . . . . . . 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 24387	. . . . . 6 ⊢ (⊤ → ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ) = ( I ↾ ℚ))
73	72	mptru 1577	. . . . 5 ⊢ ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ) = ( I ↾ ℚ)
74		recms 25701	. . . . . . . . 9 ⊢ ℝ_fld ∈ CMetSp
75	74	elexi 3473	. . . . . . . 8 ⊢ ℝ_fld ∈ V
76	5, 6	rrhval 34628	. . . . . . . 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 34652	. . . . . . . 8 ⊢ (ℚHom‘ℝ_fld) = ( I ↾ ℚ)
79	78	fveq2i 6888	. . . . . . 7 ⊢ (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘(ℚHom‘ℝ_fld)) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ))
80	77, 79	eqtri 2784	. . . . . 6 ⊢ (ℝHom‘ℝ_fld) = (((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ))
81	80	reseq1i 5966	. . . . 5 ⊢ ((ℝHom‘ℝ_fld) ↾ ℚ) = ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) ↾ ℚ)
82	73, 81, 67	3eqtr4i 2794	. . . 4 ⊢ ((ℝHom‘ℝ_fld) ↾ ℚ) = (( I ↾ ℝ) ↾ ℚ)
83	82	a1i 11	. . 3 ⊢ (⊤ → ((ℝHom‘ℝ_fld) ↾ ℚ) = (( I ↾ ℝ) ↾ ℚ))
84	1, 3, 8, 14, 83, 23, 25	hauseqcn 34530	. 2 ⊢ (⊤ → (ℝHom‘ℝ_fld) = ( I ↾ ℝ))
85	84	mptru 1577	1 ⊢ (ℝHom‘ℝ_fld) = ( I ↾ ℝ)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 {csn 4584 I cid 5545 ran crn 5652 ↾ cres 5653 “ cima 5654 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 ℝcr 11199 ℚcq 13075 (,)cioo 13476 ↾_t crest 17591 topGenctg 17608 ℝ_fldcrefld 21910 Topctop 23211 TopOnctopon 23228 clsccl 23336 neicnei 23415 Cn ccn 23542 Hauscha 23626 Regcreg 23627 Filcfil 24164 fLimf cflf 24254 CnExtccnext 24378 UnifSpcusp 24573 CUnifSpccusp 24615 CMetSpccms 25653 ℚHomcqqh 34602 ℝHomcrrh 34625 ℝExt crrext 34626

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279 ax-mulf 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-dvds 16423 df-gcd 16665 df-numer 16911 df-denom 16912 df-gz 17108 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-rest 17593 df-topn 17594 df-0g 17612 df-gsum 17613 df-topgen 17614 df-pt 17615 df-prds 17618 df-xrs 17674 df-qtop 17679 df-imas 17680 df-xps 17682 df-mre 17756 df-mrc 17757 df-acs 17759 df-proset 18468 df-poset 18487 df-plt 18502 df-toset 18589 df-ps 18740 df-tsr 18741 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-ghm 19428 df-cntz 19531 df-od 19742 df-cmn 19996 df-abl 19997 df-omnd 20335 df-ogrp 20336 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-rhm 20702 df-nzr 20763 df-subrng 20798 df-subrg 20822 df-drng 20982 df-field 20983 df-abv 21066 df-orng 21116 df-ofld 21117 df-lmod 21137 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-fbas 21675 df-fg 21676 df-metu 21677 df-cnfld 21679 df-zring 21753 df-zrh 21809 df-zlm 21810 df-chr 21811 df-refld 21911 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-nei 23416 df-cn 23545 df-cnp 23546 df-haus 23633 df-reg 23634 df-cmp 23705 df-tx 23881 df-hmeo 24074 df-fil 24165 df-fm 24257 df-flim 24258 df-flf 24259 df-fcls 24260 df-cnext 24379 df-ust 24520 df-utop 24550 df-uss 24575 df-usp 24576 df-ucn 24594 df-cfilu 24605 df-cusp 24616 df-xms 24639 df-ms 24640 df-tms 24641 df-nm 24901 df-ngp 24902 df-nrg 24904 df-nlm 24905 df-cncf 25199 df-cfil 25576 df-cmet 25578 df-cms 25656 df-qqh 34603 df-rrh 34627 df-rrext 34631

This theorem is used by: sitmcl 34983

W3C validator