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

Theorem bastg 22116
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 3436 . . . . . . . 8 𝑥 ∈ V
32pwid 4557 . . . . . . 7 𝑥 ∈ 𝒫 𝑥
43a1i 11 . . . . . 6 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ 𝒫 𝑥)
51, 4elind 4128 . . . . 5 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ (𝐵 ∩ 𝒫 𝑥))
6 elssuni 4871 . . . . 5 (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
75, 6syl 17 . . . 4 ((𝐵𝑉𝑥𝐵) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
87ex 413 . . 3 (𝐵𝑉 → (𝑥𝐵𝑥 (𝐵 ∩ 𝒫 𝑥)))
9 eltg 22107 . . 3 (𝐵𝑉 → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 (𝐵 ∩ 𝒫 𝑥)))
108, 9sylibrd 258 . 2 (𝐵𝑉 → (𝑥𝐵𝑥 ∈ (topGen‘𝐵)))
1110ssrdv 3927 1 (𝐵𝑉𝐵 ⊆ (topGen‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  cin 3886  wss 3887  𝒫 cpw 4533   cuni 4839  cfv 6433  topGenctg 17148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topgen 17154
This theorem is referenced by:  unitg  22117  tgclb  22120  tgtop  22123  tgidm  22130  tgss3  22136  bastop2  22144  elcls3  22234  ordtopn1  22345  ordtopn2  22346  leordtval2  22363  iocpnfordt  22366  icomnfordt  22367  iooordt  22368  tgcn  22403  tgcnp  22404  tgcmp  22552  2ndcsb  22600  2ndc1stc  22602  2ndcctbss  22606  2ndcomap  22609  ptopn  22734  xkoopn  22740  txopn  22753  txbasval  22757  ptpjcn  22762  flftg  23147  alexsubb  23197  blssopn  23651  iooretop  23929  bndth  24121  ovolicc2  24686  cncombf  24822  cnmbf  24823  ordtconnlem1  31874  elmbfmvol2  32234  dya2icoseg2  32245  iccllysconn  33212  rellysconn  33213  topjoin  34554  fnemeet2  34556  fnejoin1  34557  ontgval  34620  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  cnambfre  35825  kelac2  40890
  Copyright terms: Public domain W3C validator