flimss1

Description: A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ K = ⋃ K$
2	1	flimelbas	$⊢ x \in (K fLim F) \to x \in ⋃ K$
3	2	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to x \in ⋃ K$
4		simpl2	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to F \in Fil (X)$
5		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
6	4 5	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to ⋃ F = X$
7	1	flimfil	$⊢ x \in (K fLim F) \to F \in Fil (⋃ K)$
8	7	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to F \in Fil (⋃ K)$
9		filunibas	$⊢ F \in Fil (⋃ K) \to ⋃ F = ⋃ K$
10	8 9	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to ⋃ F = ⋃ K$
11	6 10	eqtr3d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to X = ⋃ K$
12	3 11	eleqtrrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to x \in X$
13		simpl1	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to J \in TopOn (X)$
14		topontop	$⊢ J \in TopOn (X) \to J \in Top$
15	13 14	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to J \in Top$
16		flimtop	$⊢ x \in (K fLim F) \to K \in Top$
17	16	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to K \in Top$
18		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
19	13 18	syl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to X = ⋃ J$
20	19 11	eqtr3d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to ⋃ J = ⋃ K$
21		simpl3	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to J \subseteq K$
22		eqid	$⊢ ⋃ J = ⋃ J$
23	22 1	topssnei	$⊢ ((J \in Top \land K \in Top \land ⋃ J = ⋃ K) \land J \subseteq K) \to nei (J) (\{x\}) \subseteq nei (K) (\{x\})$
24	15 17 20 21 23	syl31anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to nei (J) (\{x\}) \subseteq nei (K) (\{x\})$
25		flimneiss	$⊢ x \in (K fLim F) \to nei (K) (\{x\}) \subseteq F$
26	25	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to nei (K) (\{x\}) \subseteq F$
27	24 26	sstrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to nei (J) (\{x\}) \subseteq F$
28		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))$
29	13 4 28	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land nei (J) (\{x\}) \subseteq F))$
30	12 27 29	mpbir2and	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \land x \in (K fLim F)) \to x \in (J fLim F)$
31	30	ex	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \to (x \in (K fLim F) \to x \in (J fLim F))$
32	31	ssrdv	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land J \subseteq K) \to K fLim F \subseteq J fLim F$

Metamath Proof Explorer

Theorem flimss1

Proof