This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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