Definition df-tgp 21877

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

Assertion

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

Distinct variable group:   f, j

Detailed syntax breakdown of Definition df-tgp

Step	Hyp	Ref	Expression
1		ctgp 21875	. 2 class TopGrp
2		vf	. . . . . . 7 setvar f
3	2	cv 1482	. . . . . 6 class f
4		cminusg 17423	. . . . . 6 class invg
5	3, 4	cfv 5888	. . . . 5 class ( invg ` f )
6		vj	. . . . . . 7 setvar j
7	6	cv 1482	. . . . . 6 class j
8		ccn 21028	. . . . . 6 class Cn
9	7, 7, 8	co 6650	. . . . 5 class ( j Cn j )
10	5, 9	wcel 1990	. . . 4 wff ( invg ` f ) e. ( j Cn j )
11		ctopn 16082	. . . . 5 class TopOpen
12	3, 11	cfv 5888	. . . 4 class ( TopOpen ` f )
13	10, 6, 12	wsbc 3435	. . 3 wff [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j )
14		cgrp 17422	. . . 4 class Grp
15		ctmd 21874	. . . 4 class TopMnd
16	14, 15	cin 3573	. . 3 class ( Grp i^i TopMnd )
17	13, 2, 16	crab 2916	. 2 class { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }
18	1, 17	wceq 1483	1 wff TopGrp = { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }

This definition is referenced by:  istgp  21881