tgptopon - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgptopon		Structured version Visualization version GIF version

Theorem tgptopon 22682

Description: The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)

**Hypotheses**
Ref	Expression
tgpcn.j	⊢ 𝐽 = (TopOpen‘𝐺)
tgptopon.x	⊢ 𝑋 = (Base‘𝐺)

**Assertion**
Ref	Expression
tgptopon	⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))

**Proof of Theorem tgptopon**
Step	Hyp	Ref	Expression
1		tgptps 22680	. 2 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
2		tgptopon.x	. . 3 ⊢ 𝑋 = (Base‘𝐺)
3		tgpcn.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝐺)
4	2, 3	istps 21534	. 2 ⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
5	1, 4	sylib 220	1 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1531 ∈ wcel 2108 ‘cfv 6348 Basecbs 16475 TopOpenctopn 16687 TopOnctopon 21510 TopSpctps 21532 TopGrpctgp 22671

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-iota 6307 df-fun 6350 df-fv 6356 df-ov 7151 df-top 21494 df-topon 21511 df-topsp 21533 df-tmd 22672 df-tgp 22673

This theorem is referenced by: tgpsubcn 22690 tgpmulg 22693 tgpmulg2 22694 subgtgp 22705 subgntr 22707 opnsubg 22708 clssubg 22709 clsnsg 22710 cldsubg 22711 tgpconncompeqg 22712 tgpconncomp 22713 tgpconncompss 22714 snclseqg 22716 tgphaus 22717 tgpt1 22718 tgpt0 22719 qustgpopn 22720 qustgplem 22721 qustgphaus 22723 prdstgpd 22725 tgptsmscld 22751 tsmsxplem1 22753 pl1cn 31191