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 = { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctmd	⊢ TopMnd
1		vf	⊢ 𝑓
2		cmnd	⊢ Mnd
3		ctps	⊢ TopSp
4	2 3	cin	⊢ ( Mnd ∩ TopSp )
5		ctopn	⊢ TopOpen
6	1	cv	⊢ 𝑓
7	6 5	cfv	⊢ ( TopOpen ‘ 𝑓 )
8		vj	⊢ 𝑗
9		cplusf	⊢ +𝑓
10	6 9	cfv	⊢ ( +𝑓 ‘ 𝑓 )
11	8	cv	⊢ 𝑗
12		ctx	⊢ ×t
13	11 11 12	co	⊢ ( 𝑗 ×t 𝑗 )
14		ccn	⊢ Cn
15	13 11 14	co	⊢ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
16	10 15	wcel	⊢ ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
17	16 8 7	wsbc	⊢ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
18	17 1 4	crab	⊢ { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }
19	0 18	wceq	⊢ TopMnd = { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }