Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tgp Structured version   Unicode version

Definition df-tgp 18095
 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 TopMnd
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-tgp
StepHypRef Expression
1 ctgp 18093 . 2
2 vf . . . . . . 7
32cv 1651 . . . . . 6
4 cminusg 14678 . . . . . 6
53, 4cfv 5446 . . . . 5
6 vj . . . . . . 7
76cv 1651 . . . . . 6
8 ccn 17280 . . . . . 6
97, 7, 8co 6073 . . . . 5
105, 9wcel 1725 . . . 4
11 ctopn 13641 . . . . 5
123, 11cfv 5446 . . . 4
1310, 6, 12wsbc 3153 . . 3
14 cgrp 14677 . . . 4
15 ctmd 18092 . . . 4 TopMnd
1614, 15cin 3311 . . 3 TopMnd
1713, 2, 16crab 2701 . 2 TopMnd
181, 17wceq 1652 1 TopMnd
 Colors of variables: wff set class This definition is referenced by:  istgp  18099
 Copyright terms: Public domain W3C validator