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

Theorem unitg 22268
Description: The topology generated by a basis 𝐵 is a topology on 𝐵. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.)
Assertion
Ref Expression
unitg (𝐵𝑉 (topGen‘𝐵) = 𝐵)

Proof of Theorem unitg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 tg1 22265 . . . . . 6 (𝑥 ∈ (topGen‘𝐵) → 𝑥 𝐵)
2 velpw 4563 . . . . . 6 (𝑥 ∈ 𝒫 𝐵𝑥 𝐵)
31, 2sylibr 233 . . . . 5 (𝑥 ∈ (topGen‘𝐵) → 𝑥 ∈ 𝒫 𝐵)
43ssriv 3946 . . . 4 (topGen‘𝐵) ⊆ 𝒫 𝐵
5 sspwuni 5058 . . . 4 ((topGen‘𝐵) ⊆ 𝒫 𝐵 (topGen‘𝐵) ⊆ 𝐵)
64, 5mpbi 229 . . 3 (topGen‘𝐵) ⊆ 𝐵
76a1i 11 . 2 (𝐵𝑉 (topGen‘𝐵) ⊆ 𝐵)
8 bastg 22267 . . 3 (𝐵𝑉𝐵 ⊆ (topGen‘𝐵))
98unissd 4873 . 2 (𝐵𝑉 𝐵 (topGen‘𝐵))
107, 9eqssd 3959 1 (𝐵𝑉 (topGen‘𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  wss 3908  𝒫 cpw 4558   cuni 4863  cfv 6493  topGenctg 17278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6445  df-fun 6495  df-fv 6501  df-topgen 17284
This theorem is referenced by:  tgcl  22270  tgtopon  22272  tgcmp  22703  2ndcsep  22761  txtopon  22893  ptuni  22896  xkouni  22901  prdstopn  22930  tgqtop  23014  alexsubb  23348  alexsubALTlem3  23351  alexsubALTlem4  23352  ptcmplem1  23354  uniretop  24077  fneval  34755  fnemeet1  34769  kelac2  41294
  Copyright terms: Public domain W3C validator