Definition df-tmd

Description: Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

	Ref	Expression
Assertion	df-tmd	$$⊢\mathrm{TopMnd}=\left\{f\in \left(\mathrm{Mnd}\cap \mathrm{TopSp}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{+}_{𝑓}\left(f\right)\in \left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctmd	$$class\mathrm{TopMnd}$$
1		vf	$$setvarf$$
2		cmnd	$$class\mathrm{Mnd}$$
3		ctps	$$class\mathrm{TopSp}$$
4	2 3	cin	$$class\left(\mathrm{Mnd}\cap \mathrm{TopSp}\right)$$
5		ctopn	$$class\mathrm{TopOpen}$$
6	1	cv	$$setvarf$$
7	6 5	cfv	$$class\mathrm{TopOpen}\left(f\right)$$
8		vj	$$setvarj$$
9		cplusf	$$class{+}_{𝑓}$$
10	6 9	cfv	$$class{+}_{𝑓}\left(f\right)$$
11	8	cv	$$setvarj$$
12		ctx	$$class{\times }_t$$
13	11 11 12	co	$$class\left(j{\times }_{t}j\right)$$
14		ccn	$$class\mathrm{Cn}$$
15	13 11 14	co	$$class\left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)$$
16	10 15	wcel	$$wff{+}_{𝑓}\left(f\right)\in \left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)$$
17	16 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{+}_{𝑓}\left(f\right)\in \left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)$$
18	17 1 4	crab	$$class\left\{f\in \left(\mathrm{Mnd}\cap \mathrm{TopSp}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{+}_{𝑓}\left(f\right)\in \left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)\right\}$$
19	0 18	wceq	$$wff\mathrm{TopMnd}=\left\{f\in \left(\mathrm{Mnd}\cap \mathrm{TopSp}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{+}_{𝑓}\left(f\right)\in \left(\left(j{\times }_{t}j\right)\mathrm{Cn}j\right)\right\}$$