Metamath Proof Explorer

Theorem fclsss1

Description: A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

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

Proof

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