Theorem tgpgrp 24001

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 24000	. 2 ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
4	3	simp1bi 1145	1 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6527  (class class class)co 7399  TopOpenctopn 17420  Grpcgrp 18901  inv_gcminusg 18902   Cn ccn 23147  TopMndctmd 23993  TopGrpctgp 23994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5273

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-rab 3414  df-v 3459  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402  df-tgp 23996

This theorem is referenced by:  grpinvhmeo  24009  istgp2  24014  oppgtgp  24021  tgplacthmeo  24026  subgtgp  24028  subgntr  24030  opnsubg  24031  clssubg  24032  cldsubg  24034  tgpconncompeqg  24035  tgpconncomp  24036  snclseqg  24039  tgphaus  24040  tgpt1  24041  tgpt0  24042  qustgpopn  24043  qustgplem  24044  qustgphaus  24046  prdstgpd  24048  tsmsinv  24071  tsmssub  24072  tgptsmscls  24073  tsmsxplem1  24076  tsmsxplem2  24077