Theorem tgpgrp 24020

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

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
2		eqid 2734	. . 3 ⊢ (invg‘𝐺) = (invg‘𝐺)
3	1, 2	istgp 24019	. 2 ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
4	3	simp1bi 1145	1 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  TopOpenctopn 17339  Grpcgrp 18861  inv_gcminusg 18862   Cn ccn 23166  TopMndctmd 24012  TopGrpctgp 24013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-tgp 24015

This theorem is referenced by:  grpinvhmeo  24028  istgp2  24033  oppgtgp  24040  tgplacthmeo  24045  subgtgp  24047  subgntr  24049  opnsubg  24050  clssubg  24051  cldsubg  24053  tgpconncompeqg  24054  tgpconncomp  24055  snclseqg  24058  tgphaus  24059  tgpt1  24060  tgpt0  24061  qustgpopn  24062  qustgplem  24063  qustgphaus  24065  prdstgpd  24067  tsmsinv  24090  tsmssub  24091  tgptsmscls  24092  tsmsxplem1  24095  tsmsxplem2  24096