Theorem tmdcn

Description: In a topological monoid, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

	Ref	Expression
Hypotheses	tgpcn.j	|- J = ( TopOpen ` G )
	tgpcn.1	|- F = ( +f ` G )
Assertion	tmdcn	|- ( G e. TopMnd -> F e. ( ( J tX J ) Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	|- J = ( TopOpen ` G )
2		tgpcn.1	|- F = ( +f ` G )
3	2 1	istmd	|- ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ F e. ( ( J tX J ) Cn J ) ) )
4	3	simp3bi	|- ( G e. TopMnd -> F e. ( ( J tX J ) Cn J ) )