Theorem eltg3i

Description: The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(B\in V\wedge A\subseteq B\right)\to A\subseteq B$$
2		pwuni	$$⊢A\subseteq 𝒫\bigcup A$$
3		ssin	$$⊢\left(A\subseteq B\wedge A\subseteq 𝒫\bigcup A\right)\leftrightarrow A\subseteq B\cap 𝒫\bigcup A$$
4	1 2 3	sylanblc	$$⊢\left(B\in V\wedge A\subseteq B\right)\to A\subseteq B\cap 𝒫\bigcup A$$
5	4	unissd	$$⊢\left(B\in V\wedge A\subseteq B\right)\to \bigcup A\subseteq \bigcup \left(B\cap 𝒫\bigcup A\right)$$
6		eltg	$$⊢B\in V\to \left(\bigcup A\in \mathrm{topGen}\left(B\right)\leftrightarrow \bigcup A\subseteq \bigcup \left(B\cap 𝒫\bigcup A\right)\right)$$
7	6	adantr	$$⊢\left(B\in V\wedge A\subseteq B\right)\to \left(\bigcup A\in \mathrm{topGen}\left(B\right)\leftrightarrow \bigcup A\subseteq \bigcup \left(B\cap 𝒫\bigcup A\right)\right)$$
8	5 7	mpbird	$$⊢\left(B\in V\wedge A\subseteq B\right)\to \bigcup A\in \mathrm{topGen}\left(B\right)$$