| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bastg | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| bastg | ⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpr 489 | . . . . . 6 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) | |
| 2 | vex 3461 | . . . . . . . 8 ⊢ 𝑥 ∈ V | |
| 3 | 2 | pwid 4581 | . . . . . . 7 ⊢ 𝑥 ∈ 𝒫 𝑥 |
| 4 | 3 | a1i 11 | . . . . . 6 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝑥) |
| 5 | 1, 4 | elind 4155 | . . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐵 ∩ 𝒫 𝑥)) |
| 6 | elssuni 4899 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)) | |
| 7 | 5, 6 | syl 18 | . . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)) |
| 8 | 7 | ex 417 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) |
| 9 | eltg 23071 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) | |
| 10 | 8, 9 | sylibrd 262 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐵 → 𝑥 ∈ (topGen‘𝐵))) |
| 11 | 10 | ssrdv 3945 | 1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2145 ∩ cin 3906 ⊆ wss 3907 𝒫 cpw 4558 ∪ cuni 4867 ‘cfv 6525 topGenctg 17478 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-iota 6481 df-fun 6527 df-fv 6533 df-topgen 17484 |
| This theorem is referenced by: unitg 23081 tgclb 23084 tgtop 23087 tgidm 23094 tgss3 23100 bastop2 23108 elcls3 23197 ordtopn1 23308 ordtopn2 23309 leordtval2 23326 iocpnfordt 23329 icomnfordt 23330 iooordt 23331 tgcn 23366 tgcnp 23367 tgcmp 23515 2ndcsb 23563 2ndc1stc 23565 2ndcctbss 23569 2ndcomap 23572 ptopn 23697 xkoopn 23703 txopn 23716 txbasval 23720 ptpjcn 23725 flftg 24110 alexsubb 24160 blssopn 24609 iooretop 24879 bndth 25074 ovolicc2 25638 cncombf 25774 cnmbf 25775 ordtconnlem1 34226 elmbfmvol2 34569 dya2icoseg2 34580 iccllysconn 35608 rellysconn 35609 topjoin 36733 fnemeet2 36735 fnejoin1 36736 ontgval 36799 mblfinlem3 38165 mblfinlem4 38166 ismblfin 38167 cnambfre 38174 kelac2 43649 |
| Copyright terms: Public domain | W3C validator |