This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ Grp ∩ TopMnd | [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctgp class TopGrp
1 vf setvar f
2 cgrp class Grp
3 ctmd class TopMnd
4 2 3 cin class Grp ∩ TopMnd
5 ctopn class TopOpen
6 1 cv setvar f
7 6 5 cfv class TopOpen ⁡ f
8 vj setvar j
9 cminusg class inv g
10 6 9 cfv class inv g ⁡ f
11 8 cv setvar j
12 ccn class Cn
13 11 11 12 co class j Cn j
14 10 13 wcel wff inv g ⁡ f ∈ j Cn j
15 14 8 7 wsbc wff [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j
16 15 1 4 crab class f ∈ Grp ∩ TopMnd | [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j
17 0 16 wceq wff TopGrp = f ∈ Grp ∩ TopMnd | [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j