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	⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		fnetg	⊢ ( 𝐴 Fne 𝐵 → 𝐴 ⊆ ( topGen ‘ 𝐵 ) )
2	1	sselda	⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ∈ ( topGen ‘ 𝐵 ) )
3		tg2	⊢ ( ( 𝑆 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑃 ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑆 ) )
4	2 3	stoic3	⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑆 ) )