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

Theorem bastg 18530
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  |-  ( B  e.  V  ->  B  C_  ( topGen `  B )
)

Proof of Theorem bastg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 simpr 458 . . . . . 6  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  B )
2 vex 2973 . . . . . . . 8  |-  x  e. 
_V
32pwid 3871 . . . . . . 7  |-  x  e. 
~P x
43a1i 11 . . . . . 6  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  ~P x
)
51, 4elind 3537 . . . . 5  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  ( B  i^i  ~P x ) )
6 elssuni 4118 . . . . 5  |-  ( x  e.  ( B  i^i  ~P x )  ->  x  C_ 
U. ( B  i^i  ~P x ) )
75, 6syl 16 . . . 4  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  C_  U. ( B  i^i  ~P x ) )
87ex 434 . . 3  |-  ( B  e.  V  ->  (
x  e.  B  ->  x  C_  U. ( B  i^i  ~P x ) ) )
9 eltg 18521 . . 3  |-  ( B  e.  V  ->  (
x  e.  ( topGen `  B )  <->  x  C_  U. ( B  i^i  ~P x ) ) )
108, 9sylibrd 234 . 2  |-  ( B  e.  V  ->  (
x  e.  B  ->  x  e.  ( topGen `  B ) ) )
1110ssrdv 3359 1  |-  ( B  e.  V  ->  B  C_  ( topGen `  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1761    i^i cin 3324    C_ wss 3325   ~Pcpw 3857   U.cuni 4088   ` cfv 5415   topGenctg 14372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-iota 5378  df-fun 5417  df-fv 5423  df-topgen 14378
This theorem is referenced by:  unitg  18531  tgclb  18534  tgtop  18537  tgidm  18544  tgss3  18550  bastop2  18558  elcls3  18646  ordtopn1  18757  ordtopn2  18758  leordtval2  18775  iocpnfordt  18778  icomnfordt  18779  iooordt  18780  tgcn  18815  tgcnp  18816  tgcmp  18963  2ndcsb  19012  2ndc1stc  19014  2ndcctbss  19018  2ndcomap  19021  ptopn  19115  xkoopn  19121  txopn  19134  txbasval  19138  ptpjcn  19143  flftg  19528  alexsubb  19577  blssopn  20029  iooretop  20304  bndth  20489  ovolicc2  20964  cncombf  21095  cnmbf  21096  ordtconlem1  26290  elmbfmvol2  26618  dya2icoseg2  26629  iccllyscon  27069  rellyscon  27070  ontgval  28207  mblfinlem3  28355  mblfinlem4  28356  ismblfin  28357  cnambfre  28365  topjoin  28511  fnemeet2  28513  fnejoin1  28514  kelac2  29343
  Copyright terms: Public domain W3C validator