Theorem tgpgrp 24288

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 2765	. . 3 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
2		eqid 2765	. . 3 ⊢ (invg‘𝐺) = (invg‘𝐺)
3	1, 2	istgp 24287	. 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 6540  (class class class)co 7419  TopOpenctopn 17498  Grpcgrp 19046  inv_gcminusg 19047   Cn ccn 23433  TopMndctmd 24280  TopGrpctgp 24281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-tgp 24283

This theorem is used by:  grpinvhmeo  24296  istgp2  24301  oppgtgp  24308  tgplacthmeo  24313  subgtgp  24315  subgntr  24317  opnsubg  24318  clssubg  24319  cldsubg  24321  tgpconncompeqg  24322  tgpconncomp  24323  snclseqg  24326  tgphaus  24327  tgpt1  24328  tgpt0  24329  qustgpopn  24330  qustgplem  24331  qustgphaus  24333  prdstgpd  24335  tsmsinv  24358  tsmssub  24359  tgptsmscls  24360  tsmsxplem1  24363  tsmsxplem2  24364