Metamath Proof Explorer

Theorem flimss2

Description: A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	flimelbas	$⊢ x \in (J fLim G) \to x \in ⋃ J$
3	2	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to x \in ⋃ J$
4		simpl1	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to J \in TopOn (X)$
5		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
6	4 5	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to X = ⋃ J$
7	3 6	eleqtrrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to x \in X$
8		flimneiss	$⊢ x \in (J fLim G) \to nei (J) (\{x\}) \subseteq G$
9	8	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to nei (J) (\{x\}) \subseteq G$
10		simpl3	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to G \subseteq F$
11	9 10	sstrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to nei (J) (\{x\}) \subseteq F$
12		simpl2	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to F \in Fil (X)$
13		elflim	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land nei (J) (\{x\}) \subseteq F))$
14	4 12 13	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land nei (J) (\{x\}) \subseteq F))$
15	7 11 14	mpbir2and	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \land x \in (J fLim G)) \to x \in (J fLim F)$
16	15	ex	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \to (x \in (J fLim G) \to x \in (J fLim F))$
17	16	ssrdv	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land G \subseteq F) \to J fLim G \subseteq J fLim F$