![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tgpgrp | Structured version Visualization version GIF version |
Description: A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
tgpgrp | ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2731 | . . 3 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺) | |
2 | eqid 2731 | . . 3 ⊢ (invg‘𝐺) = (invg‘𝐺) | |
3 | 1, 2 | istgp 23901 | . 2 ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺)))) |
4 | 3 | simp1bi 1144 | 1 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ‘cfv 6543 (class class class)co 7412 TopOpenctopn 17374 Grpcgrp 18861 invgcminusg 18862 Cn ccn 23048 TopMndctmd 23894 TopGrpctgp 23895 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-rab 3432 df-v 3475 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-ov 7415 df-tgp 23897 |
This theorem is referenced by: grpinvhmeo 23910 istgp2 23915 oppgtgp 23922 tgplacthmeo 23927 subgtgp 23929 subgntr 23931 opnsubg 23932 clssubg 23933 cldsubg 23935 tgpconncompeqg 23936 tgpconncomp 23937 snclseqg 23940 tgphaus 23941 tgpt1 23942 tgpt0 23943 qustgpopn 23944 qustgplem 23945 qustgphaus 23947 prdstgpd 23949 tsmsinv 23972 tsmssub 23973 tgptsmscls 23974 tsmsxplem1 23977 tsmsxplem2 23978 |
Copyright terms: Public domain | W3C validator |