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		snnzg	$⊢ y \in X \to \{y\} \neq \emptyset$
24	21 23	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 \{y\} \neq \emptyset$
25		neifil	$⊢ (K \in TopOn (X) \land \{y\} \subseteq X \land \{y\} \neq \emptyset) \to nei (K) (\{y\}) \in Fil (X)$
26	15 22 24 25	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)$
27	13 14 26	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\})$
28		neiflim	$⊢ (K \in TopOn (X) \land y \in X) \to y \in (K fLim nei (K) (\{y\}))$
29	15 21 28	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\}))$
30	27 29	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\}))$
31		flimneiss	$⊢ y \in (J fLim nei (K) (\{y\})) \to nei (J) (\{y\}) \subseteq nei (K) (\{y\})$
32	30 31	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\})$
33		topontop	$⊢ J \in TopOn (X) \to J \in Top$
34	16 33	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$
35		opnneip	$⊢ (J \in Top \land x \in J \land y \in x) \to x \in nei (J) (\{y\})$
36	34 17 20 35	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\})$
37	32 36	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\})$
38	37	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\})$
39	38	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\})$
40		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)$
41		topontop	$⊢ K \in TopOn (X) \to K \in Top$
42		opnnei	$⊢ K \in Top \to (x \in K \leftrightarrow \forall y \in x x \in nei (K) (\{y\}))$
43	40 41 42	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\}))$
44	39 43	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$
45	44	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)$
46	45	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$
47	10 46	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