MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgptmd Structured version   Unicode version

Theorem tgptmd 19669
Description: A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
Assertion
Ref Expression
tgptmd  |-  ( G  e.  TopGrp  ->  G  e. TopMnd )

Proof of Theorem tgptmd
StepHypRef Expression
1 eqid 2443 . . 3  |-  ( TopOpen `  G )  =  (
TopOpen `  G )
2 eqid 2443 . . 3  |-  ( invg `  G )  =  ( invg `  G )
31, 2istgp 19667 . 2  |-  ( G  e.  TopGrp 
<->  ( G  e.  Grp  /\  G  e. TopMnd  /\  ( invg `  G )  e.  ( ( TopOpen `  G )  Cn  ( TopOpen
`  G ) ) ) )
43simp2bi 1004 1  |-  ( G  e.  TopGrp  ->  G  e. TopMnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   ` cfv 5437  (class class class)co 6110   TopOpenctopn 14379   Grpcgrp 15429   invgcminusg 15430    Cn ccn 18847  TopMndctmd 19660   TopGrpctgp 19661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-iota 5400  df-fv 5445  df-ov 6113  df-tgp 19663
This theorem is referenced by:  tgptps  19670  tgpcn  19674  tgpsubcn  19680  tgpmulg  19683  oppgtgp  19688  tgplacthmeo  19693  subgtgp  19695  clsnsg  19699  tgpt0  19708  prdstgpd  19714  tsmssub  19742  tsmsxp  19748  trgtmd2  19762  nlmtlm  20293  qqhcn  26439
  Copyright terms: Public domain W3C validator