Theorem tgpgrp 23963

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  TopOpenctopn 17325  Grpcgrp 18812  inv_gcminusg 18813   Cn ccn 23109  TopMndctmd 23955  TopGrpctgp 23956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-tgp 23958

This theorem is referenced by:  grpinvhmeo  23971  istgp2  23976  oppgtgp  23983  tgplacthmeo  23988  subgtgp  23990  subgntr  23992  opnsubg  23993  clssubg  23994  cldsubg  23996  tgpconncompeqg  23997  tgpconncomp  23998  snclseqg  24001  tgphaus  24002  tgpt1  24003  tgpt0  24004  qustgpopn  24005  qustgplem  24006  qustgphaus  24008  prdstgpd  24010  tsmsinv  24033  tsmssub  24034  tgptsmscls  24035  tsmsxplem1  24038  tsmsxplem2  24039