Metamath Proof Explorer

Theorem fclsss2

Description: A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	fclsss2	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \to J fClus G \subseteq J fClus F$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to F \subseteq G$
2		ssralv	$⊢ F \subseteq G \to (\forall s \in G x \in cls (J) (s) \to \forall s \in F x \in cls (J) (s))$
3	1 2	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to (\forall s \in G x \in cls (J) (s) \to \forall s \in F x \in cls (J) (s))$
4		simpl1	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to J \in TopOn (X)$
5		fclstopon	$⊢ x \in (J fClus G) \to (J \in TopOn (X) \leftrightarrow G \in Fil (X))$
6	5	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to (J \in TopOn (X) \leftrightarrow G \in Fil (X))$
7	4 6	mpbid	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to G \in Fil (X)$
8		isfcls2	$⊢ (J \in TopOn (X) \land G \in Fil (X)) \to (x \in (J fClus G) \leftrightarrow \forall s \in G x \in cls (J) (s))$
9	4 7 8	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to (x \in (J fClus G) \leftrightarrow \forall s \in G x \in cls (J) (s))$
10		simpl2	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to F \in Fil (X)$
11		isfcls2	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fClus F) \leftrightarrow \forall s \in F x \in cls (J) (s))$
12	4 10 11	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to (x \in (J fClus F) \leftrightarrow \forall s \in F x \in cls (J) (s))$
13	3 9 12	3imtr4d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \land x \in (J fClus G)) \to (x \in (J fClus G) \to x \in (J fClus F))$
14	13	ex	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \to (x \in (J fClus G) \to (x \in (J fClus G) \to x \in (J fClus F)))$
15	14	pm2.43d	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \to (x \in (J fClus G) \to x \in (J fClus F))$
16	15	ssrdv	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land F \subseteq G) \to J fClus G \subseteq J fClus F$