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	$$⊢\mathrm{TopGrp}=\left\{f\in \left(\mathrm{Grp}\cap \mathrm{TopMnd}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{inv}_g\left(f\right)\in \left(j\mathrm{Cn}j\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctgp	$$class\mathrm{TopGrp}$$
1		vf	$$setvarf$$
2		cgrp	$$class\mathrm{Grp}$$
3		ctmd	$$class\mathrm{TopMnd}$$
4	2 3	cin	$$class\left(\mathrm{Grp}\cap \mathrm{TopMnd}\right)$$
5		ctopn	$$class\mathrm{TopOpen}$$
6	1	cv	$$setvarf$$
7	6 5	cfv	$$class\mathrm{TopOpen}\left(f\right)$$
8		vj	$$setvarj$$
9		cminusg	$$class{inv}_g$$
10	6 9	cfv	$$class{inv}_g\left(f\right)$$
11	8	cv	$$setvarj$$
12		ccn	$$class\mathrm{Cn}$$
13	11 11 12	co	$$class\left(j\mathrm{Cn}j\right)$$
14	10 13	wcel	$$wff{inv}_g\left(f\right)\in \left(j\mathrm{Cn}j\right)$$
15	14 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{inv}_g\left(f\right)\in \left(j\mathrm{Cn}j\right)$$
16	15 1 4	crab	$$class\left\{f\in \left(\mathrm{Grp}\cap \mathrm{TopMnd}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{inv}_g\left(f\right)\in \left(j\mathrm{Cn}j\right)\right\}$$
17	0 16	wceq	$$wff\mathrm{TopGrp}=\left\{f\in \left(\mathrm{Grp}\cap \mathrm{TopMnd}\right)|\underset{\dot{}}{[}\mathrm{TopOpen}\left(f\right)/j\underset{\dot{}}{]}{inv}_g\left(f\right)\in \left(j\mathrm{Cn}j\right)\right\}$$