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 22397

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 22395	. 2 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
2		tgptopon.x	. . 3 ⊢ 𝑋 = (Base‘𝐺)
3		tgpcn.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝐺)
4	2, 3	istps 21249	. 2 ⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
5	1, 4	sylib 210	1 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ‘cfv 6190 Basecbs 16342 TopOpenctopn 16554 TopOnctopon 21225 TopSpctps 21247 TopGrpctgp 22386

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-iota 6154 df-fun 6192 df-fv 6198 df-ov 6981 df-top 21209 df-topon 21226 df-topsp 21248 df-tmd 22387 df-tgp 22388

This theorem is referenced by: tgpsubcn 22405 tgpmulg 22408 tgpmulg2 22409 subgtgp 22420 subgntr 22421 opnsubg 22422 clssubg 22423 clsnsg 22424 cldsubg 22425 tgpconncompeqg 22426 tgpconncomp 22427 tgpconncompss 22428 snclseqg 22430 tgphaus 22431 tgpt1 22432 tgpt0 22433 qustgpopn 22434 qustgplem 22435 qustgphaus 22437 prdstgpd 22439 tgptsmscld 22465 tsmsxplem1 22467 pl1cn 30842