Theorem fnetg

Description: A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Assertion	fnetg	$$⊢A\mathrm{Fne}B\to A\subseteq \mathrm{topGen}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup A=\bigcup A$$
2		eqid	$$⊢\bigcup B=\bigcup B$$
3	1 2	isfne4	$$⊢A\mathrm{Fne}B\leftrightarrow \left(\bigcup A=\bigcup B\wedge A\subseteq \mathrm{topGen}\left(B\right)\right)$$
4	3	simprbi	$$⊢A\mathrm{Fne}B\to A\subseteq \mathrm{topGen}\left(B\right)$$