Theorem fnessex

Description: If B is finer than A and S is an element of A , every point in S is an element of a subset of S which is in B . (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Assertion	fnessex	$$⊢\left(A\mathrm{Fne}B\wedge S\in A\wedge P\in S\right)\to \exists x\in B\left(P\in x\wedge x\subseteq S\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		tg2	$$⊢\left(S\in \mathrm{topGen}\left(B\right)\wedge P\in S\right)\to \exists x\in B\left(P\in x\wedge x\subseteq S\right)$$
4	2 3	stoic3	$$⊢\left(A\mathrm{Fne}B\wedge S\in A\wedge P\in S\right)\to \exists x\in B\left(P\in x\wedge x\subseteq S\right)$$