Theorem tsmsgsum 19844

Description: The convergent points of a finite topological group sum are the closure of the finite group sum operation. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by AV, 24-Jul-2019.)

Hypotheses

Ref	Expression
tsmsid.b	|- B = ( Base ` G )
tsmsid.z	|- .0. = ( 0g ` G )
tsmsid.1	|- ( ph -> G e. CMnd )
tsmsid.2	|- ( ph -> G e. TopSp )
tsmsid.a	|- ( ph -> A e. V )
tsmsid.f	|- ( ph -> F : A --> B )
tsmsid.w	|- ( ph -> F finSupp .0. )
tsmsgsum.j	|- J = ( TopOpen ` G )

Assertion

Ref	Expression
tsmsgsum	|- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { ( G gsumg F ) } ) )

Proof of Theorem tsmsgsum

Dummy variables y z u x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsmsid.2	. . . . . . 7 |- ( ph -> G e. TopSp )
2		tsmsid.b	. . . . . . . 8 |- B = ( Base ` G )
3		tsmsgsum.j	. . . . . . . 8 |- J = ( TopOpen ` G )
4	2, 3	istps 18676	. . . . . . 7 |- ( G e. TopSp <-> J e. (TopOn ` B ) )
5	1, 4	sylib 196	. . . . . 6 |- ( ph -> J e. (TopOn ` B ) )
6		toponuni 18667	. . . . . 6 |- ( J e. (TopOn ` B ) -> B = U. J )
7	5, 6	syl 16	. . . . 5 |- ( ph -> B = U. J )
8	7	eleq2d 2524	. . . 4 |- ( ph -> ( x e. B <-> x e. U. J ) )
9		elfpw 7727	. . . . . . . . . . . . . . 15 |- ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
10	9	simplbi 460	. . . . . . . . . . . . . 14 |- ( y e. ( ~P A i^i Fin ) -> y C_ A )
11	10	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
12		suppssdm 6816	. . . . . . . . . . . . . . 15 |- ( F supp .0. ) C_ dom F
13		tsmsid.f	. . . . . . . . . . . . . . . 16 |- ( ph -> F : A --> B )
14		fdm 5674	. . . . . . . . . . . . . . . 16 |- ( F : A --> B -> dom F = A )
15	13, 14	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> dom F = A )
16	12, 15	syl5sseq 3515	. . . . . . . . . . . . . 14 |- ( ph -> ( F supp .0. ) C_ A )
17	16	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ A )
18	11, 17	unssd 3643	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) C_ A )
19	9	simprbi 464	. . . . . . . . . . . . . 14 |- ( y e. ( ~P A i^i Fin ) -> y e. Fin )
20	19	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
21		tsmsid.w	. . . . . . . . . . . . . . 15 |- ( ph -> F finSupp .0. )
22	21	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F finSupp .0. )
23	22	fsuppimpd 7741	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) e. Fin )
24		unfi 7693	. . . . . . . . . . . . 13 |- ( ( y e. Fin /\ ( F supp .0. ) e. Fin ) -> ( y u. ( F supp .0. ) ) e. Fin )
25	20, 23, 24	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. Fin )
26		elfpw 7727	. . . . . . . . . . . 12 |- ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) <-> ( ( y u. ( F supp .0. ) ) C_ A /\ ( y u. ( F supp .0. ) ) e. Fin ) )
27	18, 25, 26	sylanbrc 664	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) )
28		ssun1 3630	. . . . . . . . . . . . . . 15 |- y C_ ( y u. ( F supp .0. ) )
29		id 22	. . . . . . . . . . . . . . 15 |- ( z = ( y u. ( F supp .0. ) ) -> z = ( y u. ( F supp .0. ) ) )
30	28, 29	syl5sseqr 3516	. . . . . . . . . . . . . 14 |- ( z = ( y u. ( F supp .0. ) ) -> y C_ z )
31		pm5.5 336	. . . . . . . . . . . . . 14 |- ( y C_ z -> ( ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( G gsumg ( F |` z ) ) e. u ) )
32	30, 31	syl 16	. . . . . . . . . . . . 13 |- ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( G gsumg ( F |` z ) ) e. u ) )
33		reseq2 5216	. . . . . . . . . . . . . . 15 |- ( z = ( y u. ( F supp .0. ) ) -> ( F |` z ) = ( F |` ( y u. ( F supp .0. ) ) ) )
34	33	oveq2d 6219	. . . . . . . . . . . . . 14 |- ( z = ( y u. ( F supp .0. ) ) -> ( G gsumg ( F |` z ) ) = ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) )
35	34	eleq1d 2523	. . . . . . . . . . . . 13 |- ( z = ( y u. ( F supp .0. ) ) -> ( ( G gsumg ( F |` z ) ) e. u <-> ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
36	32, 35	bitrd 253	. . . . . . . . . . . 12 |- ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
37	36	rspcv 3175	. . . . . . . . . . 11 |- ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) -> ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
38	27, 37	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) -> ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
39		tsmsid.z	. . . . . . . . . . . 12 |- .0. = ( 0g ` G )
40		tsmsid.1	. . . . . . . . . . . . 13 |- ( ph -> G e. CMnd )
41	40	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> G e. CMnd )
42		tsmsid.a	. . . . . . . . . . . . 13 |- ( ph -> A e. V )
43	42	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> A e. V )
44	13	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F : A --> B )
45		ssun2 3631	. . . . . . . . . . . . 13 |- ( F supp .0. ) C_ ( y u. ( F supp .0. ) )
46	45	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ ( y u. ( F supp .0. ) ) )
47	2, 39, 41, 43, 44, 46, 22	gsumres 16519	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) = ( G gsumg F ) )
48	47	eleq1d 2523	. . . . . . . . . 10 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( G gsumg ( F |` ( y u. ( F supp .0. ) ) ) ) e. u <-> ( G gsumg F ) e. u ) )
49	38, 48	sylibd 214	. . . . . . . . 9 |- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) -> ( G gsumg F ) e. u ) )
50	49	rexlimdva 2947	. . . . . . . 8 |- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) -> ( G gsumg F ) e. u ) )
51	21	fsuppimpd 7741	. . . . . . . . . . . 12 |- ( ph -> ( F supp .0. ) e. Fin )
52		elfpw 7727	. . . . . . . . . . . 12 |- ( ( F supp .0. ) e. ( ~P A i^i Fin ) <-> ( ( F supp .0. ) C_ A /\ ( F supp .0. ) e. Fin ) )
53	16, 51, 52	sylanbrc 664	. . . . . . . . . . 11 |- ( ph -> ( F supp .0. ) e. ( ~P A i^i Fin ) )
54	53	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) -> ( F supp .0. ) e. ( ~P A i^i Fin ) )
55	40	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> G e. CMnd )
56	42	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> A e. V )
57	13	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F : A --> B )
58		simprr 756	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( F supp .0. ) C_ z )
59	21	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F finSupp .0. )
60	2, 39, 55, 56, 57, 58, 59	gsumres 16519	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsumg ( F |` z ) ) = ( G gsumg F ) )
61		simplrr 760	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsumg F ) e. u )
62	60, 61	eqeltrd 2542	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsumg ( F |` z ) ) e. u )
63	62	expr 615	. . . . . . . . . . 11 |- ( ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F supp .0. ) C_ z -> ( G gsumg ( F |` z ) ) e. u ) )
64	63	ralrimiva 2830	. . . . . . . . . 10 |- ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) -> A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsumg ( F |` z ) ) e. u ) )
65		sseq1 3488	. . . . . . . . . . . . 13 |- ( y = ( F supp .0. ) -> ( y C_ z <-> ( F supp .0. ) C_ z ) )
66	65	imbi1d 317	. . . . . . . . . . . 12 |- ( y = ( F supp .0. ) -> ( ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( ( F supp .0. ) C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) )
67	66	ralbidv 2846	. . . . . . . . . . 11 |- ( y = ( F supp .0. ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) )
68	67	rspcev 3179	. . . . . . . . . 10 |- ( ( ( F supp .0. ) e. ( ~P A i^i Fin ) /\ A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) )
69	54, 64, 68	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( u e. J /\ ( G gsumg F ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) )
70	69	expr 615	. . . . . . . 8 |- ( ( ph /\ u e. J ) -> ( ( G gsumg F ) e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) )
71	50, 70	impbid 191	. . . . . . 7 |- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( G gsumg F ) e. u ) )
72		disjsn 4047	. . . . . . . 8 |- ( ( u i^i { ( G gsumg F ) } ) = (/) <-> -. ( G gsumg F ) e. u )
73	72	necon2abii 2718	. . . . . . 7 |- ( ( G gsumg F ) e. u <-> ( u i^i { ( G gsumg F ) } ) =/= (/) )
74	71, 73	syl6bb 261	. . . . . 6 |- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) <-> ( u i^i { ( G gsumg F ) } ) =/= (/) ) )
75	74	imbi2d 316	. . . . 5 |- ( ( ph /\ u e. J ) -> ( ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) <-> ( x e. u -> ( u i^i { ( G gsumg F ) } ) =/= (/) ) ) )
76	75	ralbidva 2844	. . . 4 |- ( ph -> ( A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) <-> A. u e. J ( x e. u -> ( u i^i { ( G gsumg F ) } ) =/= (/) ) ) )
77	8, 76	anbi12d 710	. . 3 |- ( ph -> ( ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsumg F ) } ) =/= (/) ) ) ) )
78		eqid 2454	. . . 4 |- ( ~P A i^i Fin ) = ( ~P A i^i Fin )
79	2, 3, 78, 40, 1, 42, 13	eltsms 19838	. . 3 |- ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. u ) ) ) ) )
80		topontop 18666	. . . . 5 |- ( J e. (TopOn ` B ) -> J e. Top )
81	5, 80	syl 16	. . . 4 |- ( ph -> J e. Top )
82	2, 39, 40, 42, 13, 21	gsumcl 16521	. . . . . 6 |- ( ph -> ( G gsumg F ) e. B )
83	82	snssd 4129	. . . . 5 |- ( ph -> { ( G gsumg F ) } C_ B )
84	83, 7	sseqtrd 3503	. . . 4 |- ( ph -> { ( G gsumg F ) } C_ U. J )
85		eqid 2454	. . . . 5 |- U. J = U. J
86	85	elcls2 18813	. . . 4 |- ( ( J e. Top /\ { ( G gsumg F ) } C_ U. J ) -> ( x e. ( ( cls ` J ) ` { ( G gsumg F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsumg F ) } ) =/= (/) ) ) ) )
87	81, 84, 86	syl2anc 661	. . 3 |- ( ph -> ( x e. ( ( cls ` J ) ` { ( G gsumg F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsumg F ) } ) =/= (/) ) ) ) )
88	77, 79, 87	3bitr4d 285	. 2 |- ( ph -> ( x e. ( G tsums F ) <-> x e. ( ( cls ` J ) ` { ( G gsumg F ) } ) ) )
89	88	eqrdv 2451	1 |- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { ( G gsumg F ) } ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   =/= wne 2648   A.wral 2799   E.wrex 2800   u. cun 3437   i^i cin 3438   C_ wss 3439   (/)c0 3748   ~Pcpw 3971   {csn 3988   U.cuni 4202   class class class wbr 4403   dom cdm 4951   |` cres 4953   -->wf 5525   ` cfv 5529  (class class class)co 6203   supp csupp 6803   Fincfn 7423   finSupp cfsupp 7734   Basecbs 14295   TopOpenctopn 14482   0gc0g 14500   gsum_g cgsu 14501  CMndccmn 16401   Topctop 18633  TopOnctopon 18634   TopSpctps 18636   clsccl 18757   tsums ctsu 19831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-cnex 9452  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-iin 4285  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-om 6590  df-1st 6690  df-2nd 6691  df-supp 6804  df-recs 6945  df-rdg 6979  df-1o 7033  df-oadd 7037  df-er 7214  df-map 7329  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-fsupp 7735  df-oi 7838  df-card 8223  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-nn 10437  df-n0 10694  df-z 10761  df-uz 10976  df-fz 11558  df-fzo 11669  df-seq 11927  df-hash 12224  df-0g 14502  df-gsum 14503  df-mnd 15537  df-cntz 15957  df-cmn 16403  df-fbas 17942  df-fg 17943  df-top 18638  df-topon 18641  df-topsp 18642  df-cld 18758  df-ntr 18759  df-cls 18760  df-nei 18837  df-fil 19554  df-fm 19646  df-flim 19647  df-flf 19648  df-tsms 19832

This theorem is referenced by:  tsmsid  19845  tgptsmscls  19859