Theorem bastg 23290

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.

Step	Hyp	Ref	Expression
1		simpr 490	. . . . . 6 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
2		vex 3454	. . . . . . . 8 ⊢ 𝑥 ∈ V
3	2	pwid 4580	. . . . . . 7 ⊢ 𝑥 ∈ 𝒫 𝑥
4	3	a1i 11	. . . . . 6 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝑥)
5	1, 4	elind 4097	. . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐵 ∩ 𝒫 𝑥))
6		elssuni 4898	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))
7	5, 6	syl 18	. . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))
8	7	ex 418	. . 3 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))
9		eltg 23281	. . 3 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))
10	8, 9	sylibrd 262	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐵 → 𝑥 ∈ (topGen‘𝐵)))
11	10	ssrdv 3914	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556  ∪ cuni 4866  ‘cfv 6539  topGenctg 17614

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6541  df-fv 6547  df-topgen 17620

This theorem is used by:  unitg  23291  tgclb  23294  tgtop  23297  tgidm  23304  tgss3  23310  bastop2  23318  elcls3  23407  ordtopn1  23518  ordtopn2  23519  leordtval2  23536  iocpnfordt  23539  icomnfordt  23540  iooordt  23541  tgcn  23576  tgcnp  23577  tgcmp  23725  2ndcsb  23773  2ndc1stc  23775  2ndcctbss  23780  2ndcomap  23783  ptopn  23908  xkoopn  23914  txopn  23927  txbasval  23931  ptpjcn  23936  flftg  24321  alexsubb  24371  blssopn  24820  iooretop  25090  bndth  25285  ovolicc2  25849  cncombf  25985  cnmbf  25986  ordtconnlem1  34603  elmbfmvol2  34946  dya2icoseg2  34957  iccllysconn  36102  rellysconn  36103  topjoin  37246  fnemeet2  37248  fnejoin1  37249  ontgval  37312  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  cnambfre  38680  kelac2  44161