Theorem tgpgrp 23466

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  TopOpenctopn 17317  Grpcgrp 18762  inv_gcminusg 18763   Cn ccn 22612  TopMndctmd 23458  TopGrpctgp 23459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-tgp 23461

This theorem is referenced by:  grpinvhmeo  23474  istgp2  23479  oppgtgp  23486  tgplacthmeo  23491  subgtgp  23493  subgntr  23495  opnsubg  23496  clssubg  23497  cldsubg  23499  tgpconncompeqg  23500  tgpconncomp  23501  snclseqg  23504  tgphaus  23505  tgpt1  23506  tgpt0  23507  qustgpopn  23508  qustgplem  23509  qustgphaus  23511  prdstgpd  23513  tsmsinv  23536  tsmssub  23537  tgptsmscls  23538  tsmsxplem1  23541  tsmsxplem2  23542