Theorem rrhre 26303

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

Assertion

Ref	Expression
rrhre	|- (RRHom ` RRfld ) = ( _I |` RR )

Proof of Theorem rrhre

Dummy variables a b x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniretop 20185	. . 3 |- RR = U. ( topGen ` ran (,) )
2		rehaus 20220	. . . 4 |- ( topGen ` ran (,) ) e. Haus
3	2	a1i 11	. . 3 |- ( T. -> ( topGen ` ran (,) ) e. Haus )
4		rerrext 26294	. . . 4 |- RRfld e. ℝExt
5		eqid 2435	. . . . 5 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
6		retopn 20727	. . . . 5 |- ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
7	5, 6	rrhcne 26297	. . . 4 |- (RRfld e. ℝExt -> (RRHom ` RRfld ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
8	4, 7	mp1i 12	. . 3 |- ( T. -> (RRHom ` RRfld ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
9		retop 20184	. . . . . 6 |- ( topGen ` ran (,) ) e. Top
10	1	toptopon 18382	. . . . . 6 |- ( ( topGen ` ran (,) ) e. Top <-> ( topGen ` ran (,) ) e. (TopOn ` RR ) )
11	9, 10	mpbi 208	. . . . 5 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
12		idcn 18705	. . . . 5 |- ( ( topGen ` ran (,) ) e. (TopOn ` RR ) -> ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
13	11, 12	ax-mp 5	. . . 4 |- ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) )
14	13	a1i 11	. . 3 |- ( T. -> ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
15	9	a1i 11	. . . . . . 7 |- ( T. -> ( topGen ` ran (,) ) e. Top )
16		f1oi 5666	. . . . . . . . . 10 |- ( _I |` QQ ) : QQ -1-1-onto-> QQ
17		f1of 5631	. . . . . . . . . 10 |- ( ( _I |` QQ ) : QQ -1-1-onto-> QQ -> ( _I |` QQ ) : QQ --> QQ )
18	16, 17	ax-mp 5	. . . . . . . . 9 |- ( _I |` QQ ) : QQ --> QQ
19		qssre 10953	. . . . . . . . 9 |- QQ C_ RR
20		fss 5557	. . . . . . . . 9 |- ( ( ( _I |` QQ ) : QQ --> QQ /\ QQ C_ RR ) -> ( _I |` QQ ) : QQ --> RR )
21	18, 19, 20	mp2an 667	. . . . . . . 8 |- ( _I |` QQ ) : QQ --> RR
22	21	a1i 11	. . . . . . 7 |- ( T. -> ( _I |` QQ ) : QQ --> RR )
23	19	a1i 11	. . . . . . 7 |- ( T. -> QQ C_ RR )
24		qdensere 20193	. . . . . . . 8 |- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
25	24	a1i 11	. . . . . . 7 |- ( T. -> ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR )
26	9	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( topGen ` ran (,) ) e. Top )
27		simplr 749	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> a e. ( topGen ` ran (,) ) )
28		simpr 458	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> x e. a )
29		opnneip 18567	. . . . . . . . . . . . . . . 16 |- ( ( ( topGen ` ran (,) ) e. Top /\ a e. ( topGen ` ran (,) ) /\ x e. a ) -> a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) )
30	26, 27, 28, 29	syl3anc 1213	. . . . . . . . . . . . . . 15 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) )
31		fvex 5691	. . . . . . . . . . . . . . . 16 |- ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) e. _V
32		qex 10955	. . . . . . . . . . . . . . . 16 |- QQ e. _V
33		elrestr 14352	. . . . . . . . . . . . . . . 16 |- ( ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) e. _V /\ QQ e. _V /\ a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) )
34	31, 32, 33	mp3an12 1299	. . . . . . . . . . . . . . 15 |- ( a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) )
35	30, 34	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) )
36		inss2 3561	. . . . . . . . . . . . . . . . 17 |- ( a i^i QQ ) C_ QQ
37		resiima 5173	. . . . . . . . . . . . . . . . 17 |- ( ( a i^i QQ ) C_ QQ -> ( ( _I |` QQ ) " ( a i^i QQ ) ) = ( a i^i QQ ) )
38	36, 37	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( ( _I |` QQ ) " ( a i^i QQ ) ) = ( a i^i QQ )
39		inss1 3560	. . . . . . . . . . . . . . . 16 |- ( a i^i QQ ) C_ a
40	38, 39	eqsstri 3376	. . . . . . . . . . . . . . 15 |- ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a
41	40	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a )
42		imaeq2 5155	. . . . . . . . . . . . . . . 16 |- ( b = ( a i^i QQ ) -> ( ( _I |` QQ ) " b ) = ( ( _I |` QQ ) " ( a i^i QQ ) ) )
43	42	sseq1d 3373	. . . . . . . . . . . . . . 15 |- ( b = ( a i^i QQ ) -> ( ( ( _I |` QQ ) " b ) C_ a <-> ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a ) )
44	43	rspcev 3064	. . . . . . . . . . . . . 14 |- ( ( ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) /\ ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a ) -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a )
45	35, 41, 44	syl2anc 656	. . . . . . . . . . . . 13 |- ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a )
46	45	ex 434	. . . . . . . . . . . 12 |- ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) -> ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) )
47	46	ralrimiva 2791	. . . . . . . . . . 11 |- ( x e. RR -> A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) )
48	47	ancli 548	. . . . . . . . . 10 |- ( x e. RR -> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) )
49	24	eleq2i 2499	. . . . . . . . . . . . 13 |- ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> x e. RR )
50	49	biimpri 206	. . . . . . . . . . . 12 |- ( x e. RR -> x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) )
51		trnei 19309	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ QQ C_ RR /\ x e. RR ) -> ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) e. ( Fil ` QQ ) ) )
52	11, 19, 51	mp3an12 1299	. . . . . . . . . . . 12 |- ( x e. RR -> ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) e. ( Fil ` QQ ) ) )
53	50, 52	mpbid 210	. . . . . . . . . . 11 |- ( x e. RR -> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) e. ( Fil ` QQ ) )
54		isflf 19410	. . . . . . . . . . . 12 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) e. ( Fil ` QQ ) /\ ( _I |` QQ ) : QQ --> RR ) -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
55	11, 21, 54	mp3an13 1300	. . . . . . . . . . 11 |- ( ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) e. ( Fil ` QQ ) -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
56	53, 55	syl 16	. . . . . . . . . 10 |- ( x e. RR -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
57	48, 56	mpbird 232	. . . . . . . . 9 |- ( x e. RR -> x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) )
58		ne0i 3633	. . . . . . . . 9 |- ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) -> ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) =/= (/) )
59	57, 58	syl 16	. . . . . . . 8 |- ( x e. RR -> ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) =/= (/) )
60	59	adantl 463	. . . . . . 7 |- ( ( T. /\ x e. RR ) -> ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ↾t QQ ) ) ` ( _I |` QQ ) ) =/= (/) )
61		recusp 20730	. . . . . . . . . 10 |- RRfld e. CUnifSp
62		cuspusp 19719	. . . . . . . . . 10 |- (RRfld e. CUnifSp -> RRfld e. UnifSp )
63	61, 62	ax-mp 5	. . . . . . . . 9 |- RRfld e. UnifSp
64	6	uspreg 19693	. . . . . . . . 9 |- ( (RRfld e. UnifSp /\ ( topGen ` ran (,) ) e. Haus ) -> ( topGen ` ran (,) ) e. Reg )
65	63, 2, 64	mp2an 667	. . . . . . . 8 |- ( topGen ` ran (,) ) e. Reg
66	65	a1i 11	. . . . . . 7 |- ( T. -> ( topGen ` ran (,) ) e. Reg )
67		resabs1 5129	. . . . . . . . . 10 |- ( QQ C_ RR -> ( ( _I |` RR ) |` QQ ) = ( _I |` QQ ) )
68	19, 67	ax-mp 5	. . . . . . . . 9 |- ( ( _I |` RR ) |` QQ ) = ( _I |` QQ )
69	1	cnrest 18733	. . . . . . . . . 10 |- ( ( ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) /\ QQ C_ RR ) -> ( ( _I |` RR ) |` QQ ) e. ( ( ( topGen ` ran (,) ) ↾t QQ ) Cn ( topGen ` ran (,) ) ) )
70	13, 19, 69	mp2an 667	. . . . . . . . 9 |- ( ( _I |` RR ) |` QQ ) e. ( ( ( topGen ` ran (,) ) ↾t QQ ) Cn ( topGen ` ran (,) ) )
71	68, 70	eqeltrri 2506	. . . . . . . 8 |- ( _I |` QQ ) e. ( ( ( topGen ` ran (,) ) ↾t QQ ) Cn ( topGen ` ran (,) ) )
72	71	a1i 11	. . . . . . 7 |- ( T. -> ( _I |` QQ ) e. ( ( ( topGen ` ran (,) ) ↾t QQ ) Cn ( topGen ` ran (,) ) ) )
73	1, 1, 15, 3, 22, 23, 25, 60, 66, 72	cnextfres 19484	. . . . . 6 |- ( T. -> ( ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ ) = ( _I |` QQ ) )
74	73	trud 1373	. . . . 5 |- ( ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ ) = ( _I |` QQ )
75		recms 20728	. . . . . . . . 9 |- RRfld e. CMetSp
76	75	elexi 2974	. . . . . . . 8 |- RRfld e. _V
77	5, 6	rrhval 26281	. . . . . . . 8 |- (RRfld e. _V -> (RRHom ` RRfld ) = ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` (QQHom ` RRfld ) ) )
78	76, 77	ax-mp 5	. . . . . . 7 |- (RRHom ` RRfld ) = ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` (QQHom ` RRfld ) )
79		qqhre 26302	. . . . . . . 8 |- (QQHom ` RRfld ) = ( _I |` QQ )
80	79	fveq2i 5684	. . . . . . 7 |- ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` (QQHom ` RRfld ) ) = ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) )
81	78, 80	eqtri 2455	. . . . . 6 |- (RRHom ` RRfld ) = ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) )
82	81	reseq1i 5095	. . . . 5 |- ( (RRHom ` RRfld ) |` QQ ) = ( ( ( ( topGen ` ran (,) )CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ )
83	74, 82, 68	3eqtr4i 2465	. . . 4 |- ( (RRHom ` RRfld ) |` QQ ) = ( ( _I |` RR ) |` QQ )
84	83	a1i 11	. . 3 |- ( T. -> ( (RRHom ` RRfld ) |` QQ ) = ( ( _I |` RR ) |` QQ ) )
85	1, 3, 8, 14, 84, 23, 25	hauseqcn 26181	. 2 |- ( T. -> (RRHom ` RRfld ) = ( _I |` RR ) )
86	85	trud 1373	1 |- (RRHom ` RRfld ) = ( _I |` RR )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1364   T. wtru 1365   e. wcel 1757   =/= wne 2598   A.wral 2707   E.wrex 2708   _Vcvv 2964   i^i cin 3317   C_ wss 3318   (/)c0 3627   {csn 3867   _I cid 4620   ran crn 4830   |` cres 4831   "cima 4832   -->wf 5404   -1-1-onto->wf1o 5407   ` cfv 5408  (class class class)co 6082   RRcr 9271   QQcq 10943   (,)cioo 11290   ↾_t crest 14344   topGenctg 14361  RRfldcrefld 17878   Topctop 18342  TopOnctopon 18343   clsccl 18466   neicnei 18545   Cn ccn 18672   Hauscha 18756   Regcreg 18757   Filcfil 19262   fLimf cflf 19352  CnExtccnext 19475  UnifSpcusp 19673  CUnifSpccusp 19716  CMetSpccms 20687  QQHomcqqh 26257  RRHomcrrh 26278   ℝExt crrext 26279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350  ax-addf 9351  ax-mulf 9352

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-se 4669  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6311  df-om 6468  df-1st 6568  df-2nd 6569  df-supp 6682  df-tpos 6736  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-er 7091  df-map 7206  df-pm 7207  df-ixp 7254  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-fsupp 7611  df-fi 7651  df-sup 7681  df-oi 7714  df-card 8099  df-cda 8327  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-3 10371  df-4 10372  df-5 10373  df-6 10374  df-7 10375  df-8 10376  df-9 10377  df-10 10378  df-n0 10570  df-z 10637  df-dec 10746  df-uz 10852  df-q 10944  df-rp 10982  df-xneg 11079  df-xadd 11080  df-xmul 11081  df-ioo 11294  df-ico 11296  df-icc 11297  df-fz 11427  df-fzo 11535  df-fl 11628  df-mod 11695  df-seq 11793  df-exp 11852  df-hash 12090  df-cj 12574  df-re 12575  df-im 12576  df-sqr 12710  df-abs 12711  df-dvds 13521  df-gcd 13676  df-numer 13798  df-denom 13799  df-gz 13976  df-struct 14161  df-ndx 14162  df-slot 14163  df-base 14164  df-sets 14165  df-ress 14166  df-plusg 14236  df-mulr 14237  df-starv 14238  df-sca 14239  df-vsca 14240  df-ip 14241  df-tset 14242  df-ple 14243  df-ds 14245  df-unif 14246  df-hom 14247  df-cco 14248  df-rest 14346  df-topn 14347  df-0g 14365  df-gsum 14366  df-topgen 14367  df-pt 14368  df-prds 14371  df-xrs 14425  df-qtop 14430  df-imas 14431  df-xps 14433  df-mre 14509  df-mrc 14510  df-acs 14512  df-poset 15101  df-plt 15113  df-toset 15189  df-ps 15355  df-tsr 15356  df-mnd 15400  df-mhm 15449  df-submnd 15450  df-grp 15527  df-minusg 15528  df-sbg 15529  df-mulg 15530  df-subg 15660  df-ghm 15727  df-cntz 15817  df-od 16014  df-cmn 16261  df-abl 16262  df-mgp 16568  df-rng 16582  df-cring 16583  df-ur 16584  df-oppr 16651  df-dvdsr 16669  df-unit 16670  df-invr 16700  df-dvr 16711  df-rnghom 16742  df-drng 16760  df-field 16761  df-subrg 16789  df-abv 16828  df-lmod 16876  df-nzr 17264  df-psmet 17655  df-xmet 17656  df-met 17657  df-bl 17658  df-mopn 17659  df-fbas 17660  df-fg 17661  df-metu 17663  df-cnfld 17665  df-zring 17728  df-zrh 17779  df-zlm 17780  df-chr 17781  df-refld 17879  df-top 18347  df-bases 18349  df-topon 18350  df-topsp 18351  df-cld 18467  df-ntr 18468  df-cls 18469  df-nei 18546  df-cn 18675  df-cnp 18676  df-haus 18763  df-reg 18764  df-cmp 18834  df-tx 18979  df-hmeo 19172  df-fil 19263  df-fm 19355  df-flim 19356  df-flf 19357  df-fcls 19358  df-cnext 19476  df-ust 19619  df-utop 19650  df-uss 19675  df-usp 19676  df-ucn 19695  df-cfilu 19706  df-cusp 19717  df-xms 19739  df-ms 19740  df-tms 19741  df-nm 20019  df-ngp 20020  df-nrg 20022  df-nlm 20023  df-cncf 20298  df-cfil 20610  df-cmet 20612  df-cms 20690  df-omnd 25988  df-ogrp 25989  df-orng 26120  df-ofld 26121  df-qqh 26258  df-rrh 26280  df-rrext 26284

This theorem is referenced by: (None)