Theorem fneuni

Description: If B is finer than A , every element of A is a union of elements of B . (Contributed by Jeff Hankins, 11-Oct-2009)

	Ref	Expression
Assertion	fneuni	$$⊢\left(A\mathrm{Fne}B\wedge S\in A\right)\to \exists x\left(x\subseteq B\wedge S=\bigcup x\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnetg	$$⊢A\mathrm{Fne}B\to A\subseteq \mathrm{topGen}\left(B\right)$$
2	1	sselda	$$⊢\left(A\mathrm{Fne}B\wedge S\in A\right)\to S\in \mathrm{topGen}\left(B\right)$$
3		elfvdm	$$⊢S\in \mathrm{topGen}\left(B\right)\to B\in \mathrm{dom}\mathrm{topGen}$$
4		eltg3	$$⊢B\in \mathrm{dom}\mathrm{topGen}\to \left(S\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists x\left(x\subseteq B\wedge S=\bigcup x\right)\right)$$
5	3 4	syl	$$⊢S\in \mathrm{topGen}\left(B\right)\to \left(S\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists x\left(x\subseteq B\wedge S=\bigcup x\right)\right)$$
6	5	ibi	$$⊢S\in \mathrm{topGen}\left(B\right)\to \exists x\left(x\subseteq B\wedge S=\bigcup x\right)$$
7	2 6	syl	$$⊢\left(A\mathrm{Fne}B\wedge S\in A\right)\to \exists x\left(x\subseteq B\wedge S=\bigcup x\right)$$