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

Theorem bastg 21719
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 488 . . . . . 6 ((𝐵𝑉𝑥𝐵) → 𝑥𝐵)
2 vex 3402 . . . . . . . 8 𝑥 ∈ V
32pwid 4512 . . . . . . 7 𝑥 ∈ 𝒫 𝑥
43a1i 11 . . . . . 6 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ 𝒫 𝑥)
51, 4elind 4084 . . . . 5 ((𝐵𝑉𝑥𝐵) → 𝑥 ∈ (𝐵 ∩ 𝒫 𝑥))
6 elssuni 4828 . . . . 5 (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
75, 6syl 17 . . . 4 ((𝐵𝑉𝑥𝐵) → 𝑥 (𝐵 ∩ 𝒫 𝑥))
87ex 416 . . 3 (𝐵𝑉 → (𝑥𝐵𝑥 (𝐵 ∩ 𝒫 𝑥)))
9 eltg 21710 . . 3 (𝐵𝑉 → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 (𝐵 ∩ 𝒫 𝑥)))
108, 9sylibrd 262 . 2 (𝐵𝑉 → (𝑥𝐵𝑥 ∈ (topGen‘𝐵)))
1110ssrdv 3883 1 (𝐵𝑉𝐵 ⊆ (topGen‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2114  cin 3842  wss 3843  𝒫 cpw 4488   cuni 4796  cfv 6339  topGenctg 16816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7481
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6297  df-fun 6341  df-fv 6347  df-topgen 16822
This theorem is referenced by:  unitg  21720  tgclb  21723  tgtop  21726  tgidm  21733  tgss3  21739  bastop2  21747  elcls3  21836  ordtopn1  21947  ordtopn2  21948  leordtval2  21965  iocpnfordt  21968  icomnfordt  21969  iooordt  21970  tgcn  22005  tgcnp  22006  tgcmp  22154  2ndcsb  22202  2ndc1stc  22204  2ndcctbss  22208  2ndcomap  22211  ptopn  22336  xkoopn  22342  txopn  22355  txbasval  22359  ptpjcn  22364  flftg  22749  alexsubb  22799  blssopn  23250  iooretop  23520  bndth  23712  ovolicc2  24276  cncombf  24412  cnmbf  24413  ordtconnlem1  31448  elmbfmvol2  31806  dya2icoseg2  31817  iccllysconn  32785  rellysconn  32786  topjoin  34199  fnemeet2  34201  fnejoin1  34202  ontgval  34265  mblfinlem3  35461  mblfinlem4  35462  ismblfin  35463  cnambfre  35470  kelac2  40484
  Copyright terms: Public domain W3C validator