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)\leftrightarrow 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)\leftrightarrow 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)$$