Definition df-tgp

Description: Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010)

	Ref	Expression
Assertion	df-tgp	|- TopGrp = { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctgp	|- TopGrp
1		vf	|- f
2		cgrp	|- Grp
3		ctmd	|- TopMnd
4	2 3	cin	|- ( Grp i^i TopMnd )
5		ctopn	|- TopOpen
6	1	cv	|- f
7	6 5	cfv	|- ( TopOpen ` f )
8		vj	|- j
9		cminusg	|- invg
10	6 9	cfv	|- ( invg ` f )
11	8	cv	|- j
12		ccn	|- Cn
13	11 11 12	co	|- ( j Cn j )
14	10 13	wcel	|- ( invg ` f ) e. ( j Cn j )
15	14 8 7	wsbc	|- [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j )
16	15 1 4	crab	|- { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }
17	0 16	wceq	|- TopGrp = { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }