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 24292

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 24290	. 2 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
2		tgptopon.x	. . 3 ⊢ 𝑋 = (Base‘𝐺)
3		tgpcn.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝐺)
4	2, 3	istps 23143	. 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 2146 ‘cfv 6540 Basecbs 17293 TopOpenctopn 17498 TopOnctopon 23119 TopSpctps 23141 TopGrpctgp 24281

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-iota 6496 df-fun 6542 df-fv 6548 df-ov 7422 df-top 23103 df-topon 23120 df-topsp 23142 df-tmd 24282 df-tgp 24283

This theorem is used by: tgpsubcn 24300 tgpmulg 24303 tgpmulg2 24304 subgtgp 24315 subgntr 24317 opnsubg 24318 clssubg 24319 clsnsg 24320 cldsubg 24321 tgpconncompeqg 24322 tgpconncomp 24323 tgpconncompss 24324 snclseqg 24326 tgphaus 24327 tgpt1 24328 tgpt0 24329 qustgpopn 24330 qustgplem 24331 qustgphaus 24333 prdstgpd 24335 tgptsmscld 24361 tsmsxplem1 24363 pl1cn 34411

W3C validator