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