MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgpgrp Structured version   Visualization version   GIF version

Theorem tgpgrp 21787
Description: A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
tgpgrp (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)

Proof of Theorem tgpgrp
StepHypRef Expression
1 eqid 2626 . . 3 (TopOpen‘𝐺) = (TopOpen‘𝐺)
2 eqid 2626 . . 3 (invg𝐺) = (invg𝐺)
31, 2istgp 21786 . 2 (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
43simp1bi 1074 1 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1992  cfv 5850  (class class class)co 6605  TopOpenctopn 15998  Grpcgrp 17338  invgcminusg 17339   Cn ccn 20933  TopMndctmd 21779  TopGrpctgp 21780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-tgp 21782
This theorem is referenced by:  grpinvhmeo  21795  istgp2  21800  oppgtgp  21807  tgplacthmeo  21812  subgtgp  21814  subgntr  21815  opnsubg  21816  clssubg  21817  cldsubg  21819  tgpconncompeqg  21820  tgpconncomp  21821  snclseqg  21824  tgphaus  21825  tgpt1  21826  tgpt0  21827  qustgpopn  21828  qustgplem  21829  qustgphaus  21831  prdstgpd  21833  tsmsinv  21856  tsmssub  21857  tgptsmscls  21858  tsmsxplem1  21861  tsmsxplem2  21862
  Copyright terms: Public domain W3C validator