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

Theorem bastg 21509
Description: A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
Assertion
Ref Expression
bastg (𝐵𝑉𝐵 ⊆ (topGen‘𝐵))

Proof of Theorem bastg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpr 485 . . . . . 6 ((𝐵𝑉𝑥𝐵) → 𝑥𝐵)
2 vex 3503 . . . . . . . 8 𝑥 ∈ V
32pwid 4561 . . . . . . 7 𝑥 ∈ 𝒫 𝑥
43a1i 11 . . . . . 6 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ 𝒫 𝑥)
51, 4elind 4175 . . . . 5 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ (𝐵 ∩ 𝒫 𝑥))
6 elssuni 4866 . . . . 5 (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
75, 6syl 17 . . . 4 ((𝐵𝑉𝑥𝐵) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
87ex 413 . . 3 (𝐵𝑉 → (𝑥𝐵𝑥 (𝐵 ∩ 𝒫 𝑥)))
9 eltg 21500 . . 3 (𝐵𝑉 → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 (𝐵 ∩ 𝒫 𝑥)))
108, 9sylibrd 260 . 2 (𝐵𝑉 → (𝑥𝐵𝑥 ∈ (topGen‘𝐵)))
1110ssrdv 3977 1 (𝐵𝑉𝐵 ⊆ (topGen‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  cin 3939  wss 3940  𝒫 cpw 4542   cuni 4837  cfv 6354  topGenctg 16706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fv 6362  df-topgen 16712
This theorem is referenced by:  unitg  21510  tgclb  21513  tgtop  21516  tgidm  21523  tgss3  21529  bastop2  21537  elcls3  21626  ordtopn1  21737  ordtopn2  21738  leordtval2  21755  iocpnfordt  21758  icomnfordt  21759  iooordt  21760  tgcn  21795  tgcnp  21796  tgcmp  21944  2ndcsb  21992  2ndc1stc  21994  2ndcctbss  21998  2ndcomap  22001  ptopn  22126  xkoopn  22132  txopn  22145  txbasval  22149  ptpjcn  22154  flftg  22539  alexsubb  22589  blssopn  23039  iooretop  23308  bndth  23496  ovolicc2  24057  cncombf  24193  cnmbf  24194  ordtconnlem1  31072  elmbfmvol2  31430  dya2icoseg2  31441  iccllysconn  32400  rellysconn  32401  topjoin  33616  fnemeet2  33618  fnejoin1  33619  ontgval  33682  mblfinlem3  34817  mblfinlem4  34818  ismblfin  34819  cnambfre  34826  kelac2  39549
  Copyright terms: Public domain W3C validator