Theorem tg1

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

	Ref	Expression
Assertion	tg1	$$⊢A\in \mathrm{topGen}\left(B\right)\to A\subseteq \bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢A\in \mathrm{topGen}\left(B\right)\to B\in \mathrm{dom}\mathrm{topGen}$$
2		eltg2	$$⊢B\in \mathrm{dom}\mathrm{topGen}\to \left(A\in \mathrm{topGen}\left(B\right)\leftrightarrow \left(A\subseteq \bigcup B\wedge \forall x\in A\exists y\in B\left(x\in y\wedge y\subseteq A\right)\right)\right)$$
3	2	simprbda	$$⊢\left(B\in \mathrm{dom}\mathrm{topGen}\wedge A\in \mathrm{topGen}\left(B\right)\right)\to A\subseteq \bigcup B$$
4	1 3	mpancom	$$⊢A\in \mathrm{topGen}\left(B\right)\to A\subseteq \bigcup B$$