Theorem tgpcn

Description: In a topological group, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tgpcn.j	|- J = ( TopOpen ` G )
	tgpcn.1	|- F = ( +f ` G )
Assertion	tgpcn	|- ( G e. TopGrp -> 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		tgptmd	|- ( G e. TopGrp -> G e. TopMnd )
4	1 2	tmdcn	|- ( G e. TopMnd -> F e. ( ( J tX J ) Cn J ) )
5	3 4	syl	|- ( G e. TopGrp -> F e. ( ( J tX J ) Cn J ) )