# Metamath Proof Explorer

## Theorem eltg4i

Description: An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion eltg4i ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to {A}=\bigcup \left({B}\cap 𝒫{A}\right)$

### Proof

Step Hyp Ref Expression
1 elfvdm ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to {B}\in \mathrm{dom}\mathrm{topGen}$
2 eltg ${⊢}{B}\in \mathrm{dom}\mathrm{topGen}\to \left({A}\in \mathrm{topGen}\left({B}\right)↔{A}\subseteq \bigcup \left({B}\cap 𝒫{A}\right)\right)$
3 1 2 syl ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to \left({A}\in \mathrm{topGen}\left({B}\right)↔{A}\subseteq \bigcup \left({B}\cap 𝒫{A}\right)\right)$
4 3 ibi ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to {A}\subseteq \bigcup \left({B}\cap 𝒫{A}\right)$
5 inss2 ${⊢}{B}\cap 𝒫{A}\subseteq 𝒫{A}$
6 5 unissi ${⊢}\bigcup \left({B}\cap 𝒫{A}\right)\subseteq \bigcup 𝒫{A}$
7 unipw ${⊢}\bigcup 𝒫{A}={A}$
8 6 7 sseqtri ${⊢}\bigcup \left({B}\cap 𝒫{A}\right)\subseteq {A}$
9 8 a1i ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to \bigcup \left({B}\cap 𝒫{A}\right)\subseteq {A}$
10 4 9 eqssd ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to {A}=\bigcup \left({B}\cap 𝒫{A}\right)$