Theorem tgpgrp 24452

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6566  (class class class)co 7451  TopOpenctopn 17642  Grpcgrp 19194  inv_gcminusg 19195   Cn ccn 23597  TopMndctmd 24444  TopGrpctgp 24445

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-tgp 24447

This theorem is used by:  grpinvhmeo  24460  istgp2  24465  oppgtgp  24472  tgplacthmeo  24477  subgtgp  24479  subgntr  24481  opnsubg  24482  clssubg  24483  cldsubg  24485  tgpconncompeqg  24486  tgpconncomp  24487  snclseqg  24490  tgphaus  24491  tgpt1  24492  tgpt0  24493  qustgpopn  24494  qustgplem  24495  qustgphaus  24497  prdstgpd  24499  tsmsinv  24522  tsmssub  24523  tgptsmscls  24524  tsmsxplem1  24527  tsmsxplem2  24528