Theorem tgpgrp 24409

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6546  (class class class)co 7427  TopOpenctopn 17604  Grpcgrp 19156  inv_gcminusg 19157   Cn ccn 23554  TopMndctmd 24401  TopGrpctgp 24402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-nul 5262

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3416  df-v 3455  df-sbc 3742  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-tgp 24404

This theorem is used by:  grpinvhmeo  24417  istgp2  24422  oppgtgp  24429  tgplacthmeo  24434  subgtgp  24436  subgntr  24438  opnsubg  24439  clssubg  24440  cldsubg  24442  tgpconncompeqg  24443  tgpconncomp  24444  snclseqg  24447  tgphaus  24448  tgpt1  24449  tgpt0  24450  qustgpopn  24451  qustgplem  24452  qustgphaus  24454  prdstgpd  24456  tsmsinv  24479  tsmssub  24480  tgptsmscls  24481  tsmsxplem1  24484  tsmsxplem2  24485