| 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 4900 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝒫 𝑥) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)) | |
| 7 | 5, 6 | syl 18 | . . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)) |
| 8 | 7 | ex 417 | . . 3 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) |
| 9 | eltg 23075 | . . 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 4868 ‘cfv 6525 topGenctg 17480 |
| 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 5251 ax-pow 5327 ax-pr 5395 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 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-iota 6481 df-fun 6527 df-fv 6533 df-topgen 17486 |
| This theorem is referenced by: unitg 23085 tgclb 23088 tgtop 23091 tgidm 23098 tgss3 23104 bastop2 23112 elcls3 23201 ordtopn1 23312 ordtopn2 23313 leordtval2 23330 iocpnfordt 23333 icomnfordt 23334 iooordt 23335 tgcn 23370 tgcnp 23371 tgcmp 23519 2ndcsb 23567 2ndc1stc 23569 2ndcctbss 23573 2ndcomap 23576 ptopn 23701 xkoopn 23707 txopn 23720 txbasval 23724 ptpjcn 23729 flftg 24114 alexsubb 24164 blssopn 24613 iooretop 24883 bndth 25078 ovolicc2 25642 cncombf 25778 cnmbf 25779 ordtconnlem1 34231 elmbfmvol2 34574 dya2icoseg2 34585 iccllysconn 35613 rellysconn 35614 topjoin 36738 fnemeet2 36740 fnejoin1 36741 ontgval 36804 mblfinlem3 38170 mblfinlem4 38171 ismblfin 38172 cnambfre 38179 kelac2 43654 |
| Copyright terms: Public domain | W3C validator |