Theorem tgpgrp 24138

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

Syntax hints:   → wi 4   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  TopOpenctopn 17450  Grpcgrp 18975  inv_gcminusg 18976   Cn ccn 23284  TopMndctmd 24130  TopGrpctgp 24131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-tgp 24133

This theorem is referenced by:  grpinvhmeo  24146  istgp2  24151  oppgtgp  24158  tgplacthmeo  24163  subgtgp  24165  subgntr  24167  opnsubg  24168  clssubg  24169  cldsubg  24171  tgpconncompeqg  24172  tgpconncomp  24173  snclseqg  24176  tgphaus  24177  tgpt1  24178  tgpt0  24179  qustgpopn  24180  qustgplem  24181  qustgphaus  24183  prdstgpd  24185  tsmsinv  24208  tsmssub  24209  tgptsmscls  24210  tsmsxplem1  24213  tsmsxplem2  24214