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	|- TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctmd	|- TopMnd
1		vf	|- f
2		cmnd	|- Mnd
3		ctps	|- TopSp
4	2 3	cin	|- ( Mnd i^i TopSp )
5		ctopn	|- TopOpen
6	1	cv	|- f
7	6 5	cfv	|- ( TopOpen ` f )
8		vj	|- j
9		cplusf	|- +f
10	6 9	cfv	|- ( +f ` f )
11	8	cv	|- j
12		ctx	|- tX
13	11 11 12	co	|- ( j tX j )
14		ccn	|- Cn
15	13 11 14	co	|- ( ( j tX j ) Cn j )
16	10 15	wcel	|- ( +f ` f ) e. ( ( j tX j ) Cn j )
17	16 8 7	wsbc	|- [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j )
18	17 1 4	crab	|- { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }
19	0 18	wceq	|- TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }