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 24314

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ‘cfv 6537 Basecbs 17307 TopOpenctopn 17512 TopOnctopon 23141 TopSpctps 23163 TopGrpctgp 24303

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740

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-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-sbc 3743 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-iota 6493 df-fun 6539 df-fv 6545 df-ov 7420 df-top 23125 df-topon 23142 df-topsp 23164 df-tmd 24304 df-tgp 24305

This theorem is used by: tgpsubcn 24322 tgpmulg 24325 tgpmulg2 24326 subgtgp 24337 subgntr 24339 opnsubg 24340 clssubg 24341 clsnsg 24342 cldsubg 24343 tgpconncompeqg 24344 tgpconncomp 24345 tgpconncompss 24346 snclseqg 24348 tgphaus 24349 tgpt1 24350 tgpt0 24351 qustgpopn 24352 qustgplem 24353 qustgphaus 24355 prdstgpd 24357 tgptsmscld 24383 tsmsxplem1 24385 pl1cn 34473

W3C validator