This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \land S \in A \land P \in S) \to \exists x \in B (P \in x \land x \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		fnetg	$⊢ A Fne B \to A \subseteq topGen (B)$
2	1	sselda	$⊢ (A Fne B \land S \in A) \to S \in topGen (B)$
3		tg2	$⊢ (S \in topGen (B) \land P \in S) \to \exists x \in B (P \in x \land x \subseteq S)$
4	2 3	stoic3	$⊢ (A Fne B \land S \in A \land P \in S) \to \exists x \in B (P \in x \land x \subseteq S)$