Theorem efopnlem2 23506

Description: Lemma for efopn 23507. (Contributed by Mario Carneiro, 2-May-2015.)

Hypothesis

Ref	Expression
efopn.j	|- J = ( TopOpen ` ℂfld )

Assertion

Ref	Expression
efopnlem2	|- ( ( R e. RR+ /\ R < pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J )

Proof of Theorem efopnlem2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		logf1o 23418	. . . . . . . 8 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
2		f1orn 5832	. . . . . . . . 9 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> ( log Fn ( CC \ { 0 } ) /\ Fun `' log ) )
3	2	simprbi 465	. . . . . . . 8 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> Fun `' log )
4		funcnvres 5661	. . . . . . . 8 |- ( Fun `' log -> `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) )
5	1, 3, 4	mp2b 10	. . . . . . 7 |- `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
6		df-log 23410	. . . . . . . . . 10 |- log = `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
7	6	cnveqi 5020	. . . . . . . . 9 |- `' log = `' `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
8		relres 5143	. . . . . . . . . 10 |- Rel ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
9		dfrel2 5297	. . . . . . . . . 10 |- ( Rel ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) <-> `' `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) = ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) )
10	8, 9	mpbi 211	. . . . . . . . 9 |- `' `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) = ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
11	7, 10	eqtri 2449	. . . . . . . 8 |- `' log = ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
12	11	reseq1i 5112	. . . . . . 7 |- ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
13		imassrn 5190	. . . . . . . . 9 |- ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ran log
14		logrn 23412	. . . . . . . . 9 |- ran log = ( `' Im " ( -u pi (,] pi ) )
15	13, 14	sseqtri 3493	. . . . . . . 8 |- ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ( `' Im " ( -u pi (,] pi ) )
16		resabs1 5144	. . . . . . . 8 |- ( ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ( `' Im " ( -u pi (,] pi ) ) -> ( ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) )
17	15, 16	ax-mp 5	. . . . . . 7 |- ( ( exp |` ( `' Im " ( -u pi (,] pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
18	5, 12, 17	3eqtri 2453	. . . . . 6 |- `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
19	18	imaeq1i 5176	. . . . 5 |- ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) )
20		cnxmet 21730	. . . . . . . . . . . . 13 |- ( abs o. - ) e. ( *Met ` CC )
21	20	a1i 11	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ R < pi ) -> ( abs o. - ) e. ( *Met ` CC ) )
22		0cnd 9625	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ R < pi ) -> 0 e. CC )
23		rpxr 11298	. . . . . . . . . . . . 13 |- ( R e. RR+ -> R e. RR* )
24	23	adantr 466	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ R < pi ) -> R e. RR* )
25		blssm 21370	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ CC )
26	21, 22, 24, 25	syl3anc 1264	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ R < pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ CC )
27	26	sselda 3461	. . . . . . . . . 10 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> x e. CC )
28	27	imcld 13226	. . . . . . . . . . 11 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) e. RR )
29		efopnlem1 23505	. . . . . . . . . . . . 13 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` x ) ) < pi )
30		pire 23317	. . . . . . . . . . . . . 14 |- pi e. RR
31		abslt 13345	. . . . . . . . . . . . . 14 |- ( ( ( Im ` x ) e. RR /\ pi e. RR ) -> ( ( abs ` ( Im ` x ) ) < pi <-> ( -u pi < ( Im ` x ) /\ ( Im ` x ) < pi ) ) )
32	28, 30, 31	sylancl 666	. . . . . . . . . . . . 13 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( ( abs ` ( Im ` x ) ) < pi <-> ( -u pi < ( Im ` x ) /\ ( Im ` x ) < pi ) ) )
33	29, 32	mpbid 213	. . . . . . . . . . . 12 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( -u pi < ( Im ` x ) /\ ( Im ` x ) < pi ) )
34	33	simpld 460	. . . . . . . . . . 11 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> -u pi < ( Im ` x ) )
35	33	simprd 464	. . . . . . . . . . 11 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) < pi )
36	30	renegcli 9924	. . . . . . . . . . . . 13 |- -u pi e. RR
37	36	rexri 9682	. . . . . . . . . . . 12 |- -u pi e. RR*
38	30	rexri 9682	. . . . . . . . . . . 12 |- pi e. RR*
39		elioo2 11666	. . . . . . . . . . . 12 |- ( ( -u pi e. RR* /\ pi e. RR* ) -> ( ( Im ` x ) e. ( -u pi (,) pi ) <-> ( ( Im ` x ) e. RR /\ -u pi < ( Im ` x ) /\ ( Im ` x ) < pi ) ) )
40	37, 38, 39	mp2an 676	. . . . . . . . . . 11 |- ( ( Im ` x ) e. ( -u pi (,) pi ) <-> ( ( Im ` x ) e. RR /\ -u pi < ( Im ` x ) /\ ( Im ` x ) < pi ) )
41	28, 34, 35, 40	syl3anbrc 1189	. . . . . . . . . 10 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) e. ( -u pi (,) pi ) )
42		imf 13144	. . . . . . . . . . 11 |- Im : CC --> RR
43		ffn 5737	. . . . . . . . . . 11 |- ( Im : CC --> RR -> Im Fn CC )
44		elpreima 6008	. . . . . . . . . . 11 |- ( Im Fn CC -> ( x e. ( `' Im " ( -u pi (,) pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u pi (,) pi ) ) ) )
45	42, 43, 44	mp2b 10	. . . . . . . . . 10 |- ( x e. ( `' Im " ( -u pi (,) pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u pi (,) pi ) ) )
46	27, 41, 45	sylanbrc 668	. . . . . . . . 9 |- ( ( ( R e. RR+ /\ R < pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> x e. ( `' Im " ( -u pi (,) pi ) ) )
47	46	ex 435	. . . . . . . 8 |- ( ( R e. RR+ /\ R < pi ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) R ) -> x e. ( `' Im " ( -u pi (,) pi ) ) ) )
48	47	ssrdv 3467	. . . . . . 7 |- ( ( R e. RR+ /\ R < pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( `' Im " ( -u pi (,) pi ) ) )
49		df-ima 4858	. . . . . . . 8 |- ( log " ( CC \ ( -oo (,] 0 ) ) ) = ran ( log |` ( CC \ ( -oo (,] 0 ) ) )
50		eqid 2420	. . . . . . . . . 10 |- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
51	50	logf1o2 23499	. . . . . . . . 9 |- ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -1-1-onto-> ( `' Im " ( -u pi (,) pi ) )
52		f1ofo 5829	. . . . . . . . 9 |- ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -1-1-onto-> ( `' Im " ( -u pi (,) pi ) ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -onto-> ( `' Im " ( -u pi (,) pi ) ) )
53		forn 5804	. . . . . . . . 9 |- ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -onto-> ( `' Im " ( -u pi (,) pi ) ) -> ran ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u pi (,) pi ) ) )
54	51, 52, 53	mp2b 10	. . . . . . . 8 |- ran ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u pi (,) pi ) )
55	49, 54	eqtri 2449	. . . . . . 7 |- ( log " ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u pi (,) pi ) )
56	48, 55	syl6sseqr 3508	. . . . . 6 |- ( ( R e. RR+ /\ R < pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( log " ( CC \ ( -oo (,] 0 ) ) ) )
57		resima2 5149	. . . . . 6 |- ( ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( log " ( CC \ ( -oo (,] 0 ) ) ) -> ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
58	56, 57	syl 17	. . . . 5 |- ( ( R e. RR+ /\ R < pi ) -> ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
59	19, 58	syl5eq 2473	. . . 4 |- ( ( R e. RR+ /\ R < pi ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
60	50	logcn 23496	. . . . . 6 |- ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
61		difss 3589	. . . . . . 7 |- ( CC \ ( -oo (,] 0 ) ) C_ CC
62		ssid 3480	. . . . . . 7 |- CC C_ CC
63		efopn.j	. . . . . . . 8 |- J = ( TopOpen ` ℂfld )
64		eqid 2420	. . . . . . . 8 |- ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) = ( J ↾t ( CC \ ( -oo (,] 0 ) ) )
65	63	cnfldtop 21741	. . . . . . . . . 10 |- J e. Top
66	63	cnfldtopon 21740	. . . . . . . . . . . 12 |- J e. (TopOn ` CC )
67	66	toponunii 19884	. . . . . . . . . . 11 |- CC = U. J
68	67	restid 15292	. . . . . . . . . 10 |- ( J e. Top -> ( J ↾t CC ) = J )
69	65, 68	ax-mp 5	. . . . . . . . 9 |- ( J ↾t CC ) = J
70	69	eqcomi 2433	. . . . . . . 8 |- J = ( J ↾t CC )
71	63, 64, 70	cncfcn 21863	. . . . . . 7 |- ( ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ CC C_ CC ) -> ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) Cn J ) )
72	61, 62, 71	mp2an 676	. . . . . 6 |- ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) Cn J )
73	60, 72	eleqtri 2506	. . . . 5 |- ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) Cn J )
74	63	cnfldtopn 21739	. . . . . . 7 |- J = ( MetOpen ` ( abs o. - ) )
75	74	blopn 21452	. . . . . 6 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) R ) e. J )
76	21, 22, 24, 75	syl3anc 1264	. . . . 5 |- ( ( R e. RR+ /\ R < pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) e. J )
77		cnima 20218	. . . . 5 |- ( ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) Cn J ) /\ ( 0 ( ball ` ( abs o. - ) ) R ) e. J ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) )
78	73, 76, 77	sylancr 667	. . . 4 |- ( ( R e. RR+ /\ R < pi ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) )
79	59, 78	eqeltrrd 2509	. . 3 |- ( ( R e. RR+ /\ R < pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) )
80	50	logdmopn 23498	. . . . 5 |- ( CC \ ( -oo (,] 0 ) ) e. ( TopOpen ` ℂfld )
81	80, 63	eleqtrri 2507	. . . 4 |- ( CC \ ( -oo (,] 0 ) ) e. J
82		restopn2 20130	. . . 4 |- ( ( J e. Top /\ ( CC \ ( -oo (,] 0 ) ) e. J ) -> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) <-> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) ) )
83	65, 81, 82	mp2an 676	. . 3 |- ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J ↾t ( CC \ ( -oo (,] 0 ) ) ) <-> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) )
84	79, 83	sylib 199	. 2 |- ( ( R e. RR+ /\ R < pi ) -> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) )
85	84	simpld 460	1 |- ( ( R e. RR+ /\ R < pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1867   \ cdif 3430   C_ wss 3433   {csn 3993   class class class wbr 4417   `'ccnv 4844   ran crn 4846   |` cres 4847   "cima 4848   o. ccom 4849   Rel wrel 4850   Fun wfun 5586   Fn wfn 5587   -->wf 5588   -onto->wfo 5590   -1-1-onto->wf1o 5591   ` cfv 5592  (class class class)co 6296   CCcc 9526   RRcr 9527   0cc0 9528   -oocmnf 9662   RR*cxr 9663   < clt 9664   - cmin 9849   -ucneg 9850   RR+crp 11291   (,)cioo 11624   (,]cioc 11625   Imcim 13129   abscabs 13265   expce 14081   picpi 14086   ↾_t crest 15279   TopOpenctopn 15280   *Metcxmt 18896   ballcbl 18898  ℂ_fldccnfld 18911   Topctop 19854   Cn ccn 20177   -cn->ccncf 21830   logclog 23408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-inf2 8137  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605  ax-pre-sup 9606  ax-addf 9607  ax-mulf 9608

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-se 4805  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6536  df-om 6698  df-1st 6798  df-2nd 6799  df-supp 6917  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-2o 7182  df-oadd 7185  df-er 7362  df-map 7473  df-pm 7474  df-ixp 7522  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-fsupp 7881  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8016  df-card 8363  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-4 10659  df-5 10660  df-6 10661  df-7 10662  df-8 10663  df-9 10664  df-10 10665  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-ioo 11628  df-ioc 11629  df-ico 11630  df-icc 11631  df-fz 11772  df-fzo 11903  df-fl 12014  df-mod 12083  df-seq 12200  df-exp 12259  df-fac 12446  df-bc 12474  df-hash 12502  df-shft 13098  df-cj 13130  df-re 13131  df-im 13132  df-sqrt 13266  df-abs 13267  df-limsup 13493  df-clim 13519  df-rlim 13520  df-sum 13720  df-ef 14088  df-sin 14090  df-cos 14091  df-tan 14092  df-pi 14093  df-struct 15083  df-ndx 15084  df-slot 15085  df-base 15086  df-sets 15087  df-ress 15088  df-plusg 15163  df-mulr 15164  df-starv 15165  df-sca 15166  df-vsca 15167  df-ip 15168  df-tset 15169  df-ple 15170  df-ds 15172  df-unif 15173  df-hom 15174  df-cco 15175  df-rest 15281  df-topn 15282  df-0g 15300  df-gsum 15301  df-topgen 15302  df-pt 15303  df-prds 15306  df-xrs 15360  df-qtop 15365  df-imas 15366  df-xps 15368  df-mre 15444  df-mrc 15445  df-acs 15447  df-mgm 16440  df-sgrp 16479  df-mnd 16489  df-submnd 16535  df-mulg 16628  df-cntz 16923  df-cmn 17373  df-psmet 18903  df-xmet 18904  df-met 18905  df-bl 18906  df-mopn 18907  df-fbas 18908  df-fg 18909  df-cnfld 18912  df-top 19858  df-bases 19859  df-topon 19860  df-topsp 19861  df-cld 19971  df-ntr 19972  df-cls 19973  df-nei 20051  df-lp 20089  df-perf 20090  df-cn 20180  df-cnp 20181  df-haus 20268  df-cmp 20339  df-tx 20514  df-hmeo 20707  df-fil 20798  df-fm 20890  df-flim 20891  df-flf 20892  df-xms 21272  df-ms 21273  df-tms 21274  df-cncf 21832  df-limc 22728  df-dv 22729  df-log 23410

This theorem is referenced by:  efopn  23507