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

Theorem bastg 18590
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 461 . . . . . 6  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  B )
2 vex 2994 . . . . . . . 8  |-  x  e. 
_V
32pwid 3893 . . . . . . 7  |-  x  e. 
~P x
43a1i 11 . . . . . 6  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  ~P x
)
51, 4elind 3559 . . . . 5  |-  ( ( B  e.  V  /\  x  e.  B )  ->  x  e.  ( B  i^i  ~P x ) )
6 elssuni 4140 . . . . 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 18581 . . 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 3381 1  |-  ( B  e.  V  ->  B  C_  ( topGen `  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    i^i cin 3346    C_ wss 3347   ~Pcpw 3879   U.cuni 4110   ` cfv 5437   topGenctg 14395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-opab 4370  df-mpt 4371  df-id 4655  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-iota 5400  df-fun 5439  df-fv 5445  df-topgen 14401
This theorem is referenced by:  unitg  18591  tgclb  18594  tgtop  18597  tgidm  18604  tgss3  18610  bastop2  18618  elcls3  18706  ordtopn1  18817  ordtopn2  18818  leordtval2  18835  iocpnfordt  18838  icomnfordt  18839  iooordt  18840  tgcn  18875  tgcnp  18876  tgcmp  19023  2ndcsb  19072  2ndc1stc  19074  2ndcctbss  19078  2ndcomap  19081  ptopn  19175  xkoopn  19181  txopn  19194  txbasval  19198  ptpjcn  19203  flftg  19588  alexsubb  19637  blssopn  20089  iooretop  20364  bndth  20549  ovolicc2  21024  cncombf  21155  cnmbf  21156  ordtconlem1  26373  elmbfmvol2  26701  dya2icoseg2  26712  iccllyscon  27158  rellyscon  27159  ontgval  28296  mblfinlem3  28453  mblfinlem4  28454  ismblfin  28455  cnambfre  28463  topjoin  28609  fnemeet2  28611  fnejoin1  28612  kelac2  29441
  Copyright terms: Public domain W3C validator