flimcf

Description: Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	flimcf	$⊢ (J \in TopOn (X) \land K \in TopOn (X)) \to (J \subseteq K \leftrightarrow \forall f \in Fil (X) K fLim f \subseteq J fLim f)$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to J \in TopOn (X)$
2		simprl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to f \in Fil (X)$
3		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to J \subseteq K$
4		flimss1	$⊢ (J \in TopOn (X) \land f \in Fil (X) \land J \subseteq K) \to K fLim f \subseteq J fLim f$
5	1 2 3 4	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to K fLim f \subseteq J fLim f$
6		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to x \in (K fLim f)$
7	5 6	sseldd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land (f \in Fil (X) \land x \in (K fLim f))) \to x \in (J fLim f)$
8	7	expr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land f \in Fil (X)) \to (x \in (K fLim f) \to x \in (J fLim f))$
9	8	ssrdv	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \land f \in Fil (X)) \to K fLim f \subseteq J fLim f$
10	9	ralrimiva	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \to \forall f \in Fil (X) K fLim f \subseteq J fLim f$
11		oveq2	$⊢ f = nei (K) (\{y\}) \to K fLim f = K fLim nei (K) (\{y\})$
12		oveq2	$⊢ f = nei (K) (\{y\}) \to J fLim f = J fLim nei (K) (\{y\})$
13	11 12	sseq12d	$⊢ f = nei (K) (\{y\}) \to (K fLim f \subseteq J fLim f \leftrightarrow K fLim nei (K) (\{y\}) \subseteq J fLim nei (K) (\{y\}))$
14		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to \forall f \in Fil (X) K fLim f \subseteq J fLim f$
15		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to K \in TopOn (X)$
16		simplll	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to J \in TopOn (X)$
17		simprl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to x \in J$
18		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
19	16 17 18	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to x \subseteq X$
20		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to y \in x$
21	19 20	sseldd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to y \in X$
22	21	snssd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to \{y\} \subseteq X$
23	20	snn0d	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to \{y\} \neq \emptyset$
24		neifil	$⊢ (K \in TopOn (X) \land \{y\} \subseteq X \land \{y\} \neq \emptyset) \to nei (K) (\{y\}) \in Fil (X)$
25	15 22 23 24	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to nei (K) (\{y\}) \in Fil (X)$
26	13 14 25	rspcdva	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to K fLim nei (K) (\{y\}) \subseteq J fLim nei (K) (\{y\})$
27		neiflim	$⊢ (K \in TopOn (X) \land y \in X) \to y \in (K fLim nei (K) (\{y\}))$
28	15 21 27	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to y \in (K fLim nei (K) (\{y\}))$
29	26 28	sseldd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to y \in (J fLim nei (K) (\{y\}))$
30		flimneiss	$⊢ y \in (J fLim nei (K) (\{y\})) \to nei (J) (\{y\}) \subseteq nei (K) (\{y\})$
31	29 30	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to nei (J) (\{y\}) \subseteq nei (K) (\{y\})$
32		topontop	$⊢ J \in TopOn (X) \to J \in Top$
33	16 32	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to J \in Top$
34		opnneip	$⊢ (J \in Top \land x \in J \land y \in x) \to x \in nei (J) (\{y\})$
35	33 17 20 34	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to x \in nei (J) (\{y\})$
36	31 35	sseldd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land (x \in J \land y \in x)) \to x \in nei (K) (\{y\})$
37	36	anassrs	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land x \in J) \land y \in x) \to x \in nei (K) (\{y\})$
38	37	ralrimiva	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land x \in J) \to \forall y \in x x \in nei (K) (\{y\})$
39		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land x \in J) \to K \in TopOn (X)$
40		topontop	$⊢ K \in TopOn (X) \to K \in Top$
41		opnnei	$⊢ K \in Top \to (x \in K \leftrightarrow \forall y \in x x \in nei (K) (\{y\}))$
42	39 40 41	3syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land x \in J) \to (x \in K \leftrightarrow \forall y \in x x \in nei (K) (\{y\}))$
43	38 42	mpbird	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \land x \in J) \to x \in K$
44	43	ex	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \to (x \in J \to x \in K)$
45	44	ssrdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fLim f \subseteq J fLim f) \to J \subseteq K$
46	10 45	impbida	$⊢ (J \in TopOn (X) \land K \in TopOn (X)) \to (J \subseteq K \leftrightarrow \forall f \in Fil (X) K fLim f \subseteq J fLim f)$

Metamath Proof Explorer

Theorem flimcf

Proof