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	|- ( ( A Fne B /\ S e. A /\ P e. S ) -> E. x e. B ( P e. x /\ x C_ S ) )

Proof

Step	Hyp	Ref	Expression
1		fnetg	|- ( A Fne B -> A C_ ( topGen ` B ) )
2	1	sselda	|- ( ( A Fne B /\ S e. A ) -> S e. ( topGen ` B ) )
3		tg2	|- ( ( S e. ( topGen ` B ) /\ P e. S ) -> E. x e. B ( P e. x /\ x C_ S ) )
4	2 3	stoic3	|- ( ( A Fne B /\ S e. A /\ P e. S ) -> E. x e. B ( P e. x /\ x C_ S ) )