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

Theorem tgpgrp 23006
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 2739 . . 3 (TopOpen‘𝐺) = (TopOpen‘𝐺)
2 eqid 2739 . . 3 (invg𝐺) = (invg𝐺)
31, 2istgp 23005 . 2 (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
43simp1bi 1147 1 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cfv 6400  (class class class)co 7234  TopOpenctopn 16958  Grpcgrp 18397  invgcminusg 18398   Cn ccn 22152  TopMndctmd 22998  TopGrpctgp 22999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-nul 5215
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-iota 6358  df-fv 6408  df-ov 7237  df-tgp 23001
This theorem is referenced by:  grpinvhmeo  23014  istgp2  23019  oppgtgp  23026  tgplacthmeo  23031  subgtgp  23033  subgntr  23035  opnsubg  23036  clssubg  23037  cldsubg  23039  tgpconncompeqg  23040  tgpconncomp  23041  snclseqg  23044  tgphaus  23045  tgpt1  23046  tgpt0  23047  qustgpopn  23048  qustgplem  23049  qustgphaus  23051  prdstgpd  23053  tsmsinv  23076  tsmssub  23077  tgptsmscls  23078  tsmsxplem1  23081  tsmsxplem2  23082
  Copyright terms: Public domain W3C validator