Definition df-tmd 21876

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.)

Assertion

Ref	Expression
df-tmd	|- TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }

Distinct variable group:   f, j

Detailed syntax breakdown of Definition df-tmd

Step	Hyp	Ref	Expression
1		ctmd 21874	. 2 class TopMnd
2		vf	. . . . . . 7 setvar f
3	2	cv 1482	. . . . . 6 class f
4		cplusf 17239	. . . . . 6 class +f
5	3, 4	cfv 5888	. . . . 5 class ( +f ` f )
6		vj	. . . . . . . 8 setvar j
7	6	cv 1482	. . . . . . 7 class j
8		ctx 21363	. . . . . . 7 class tX
9	7, 7, 8	co 6650	. . . . . 6 class ( j tX j )
10		ccn 21028	. . . . . 6 class Cn
11	9, 7, 10	co 6650	. . . . 5 class ( ( j tX j ) Cn j )
12	5, 11	wcel 1990	. . . 4 wff ( +f ` f ) e. ( ( j tX j ) Cn j )
13		ctopn 16082	. . . . 5 class TopOpen
14	3, 13	cfv 5888	. . . 4 class ( TopOpen ` f )
15	12, 6, 14	wsbc 3435	. . 3 wff [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j )
16		cmnd 17294	. . . 4 class Mnd
17		ctps 20736	. . . 4 class TopSp
18	16, 17	cin 3573	. . 3 class ( Mnd i^i TopSp )
19	15, 2, 18	crab 2916	. 2 class { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }
20	1, 19	wceq 1483	1 wff TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }

This definition is referenced by:  istmd  21878