fcfnei

Description: The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	fcfnei	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		isfcf	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset)))$
2		simpll1	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to J \in TopOn (X)$
3		topontop	$⊢ J \in TopOn (X) \to J \in Top$
4	2 3	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to J \in Top$
5		simpr	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to n \in nei (J) (\{A\})$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	neii1	$⊢ (J \in Top \land n \in nei (J) (\{A\})) \to n \subseteq ⋃ J$
8	4 5 7	syl2anc	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to n \subseteq ⋃ J$
9	6	ntrss2	$⊢ (J \in Top \land n \subseteq ⋃ J) \to int (J) (n) \subseteq n$
10	4 8 9	syl2anc	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to int (J) (n) \subseteq n$
11		simplr	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to A \in X$
12		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
13	2 12	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to X = ⋃ J$
14	11 13	eleqtrd	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to A \in ⋃ J$
15	14	snssd	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to \{A\} \subseteq ⋃ J$
16	6	neiint	$⊢ (J \in Top \land \{A\} \subseteq ⋃ J \land n \subseteq ⋃ J) \to (n \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (n))$
17	4 15 8 16	syl3anc	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to (n \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (n))$
18	5 17	mpbid	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to \{A\} \subseteq int (J) (n)$
19		snssg	$⊢ A \in X \to (A \in int (J) (n) \leftrightarrow \{A\} \subseteq int (J) (n))$
20	11 19	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to (A \in int (J) (n) \leftrightarrow \{A\} \subseteq int (J) (n))$
21	18 20	mpbird	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to A \in int (J) (n)$
22	6	ntropn	$⊢ (J \in Top \land n \subseteq ⋃ J) \to int (J) (n) \in J$
23	4 8 22	syl2anc	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to int (J) (n) \in J$
24		eleq2	$⊢ o = int (J) (n) \to (A \in o \leftrightarrow A \in int (J) (n))$
25		ineq1	$⊢ o = int (J) (n) \to o \cap F [s] = int (J) (n) \cap F [s]$
26	25	neeq1d	$⊢ o = int (J) (n) \to (o \cap F [s] \neq \emptyset \leftrightarrow int (J) (n) \cap F [s] \neq \emptyset)$
27	26	ralbidv	$⊢ o = int (J) (n) \to (\forall s \in L o \cap F [s] \neq \emptyset \leftrightarrow \forall s \in L int (J) (n) \cap F [s] \neq \emptyset)$
28	24 27	imbi12d	$⊢ o = int (J) (n) \to ((A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \leftrightarrow (A \in int (J) (n) \to \forall s \in L int (J) (n) \cap F [s] \neq \emptyset))$
29	28	rspcv	$⊢ int (J) (n) \in J \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \to (A \in int (J) (n) \to \forall s \in L int (J) (n) \cap F [s] \neq \emptyset))$
30	23 29	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \to (A \in int (J) (n) \to \forall s \in L int (J) (n) \cap F [s] \neq \emptyset))$
31	21 30	mpid	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \to \forall s \in L int (J) (n) \cap F [s] \neq \emptyset)$
32		ssrin	$⊢ int (J) (n) \subseteq n \to int (J) (n) \cap F [s] \subseteq n \cap F [s]$
33		ssn0	$⊢ (int (J) (n) \cap F [s] \subseteq n \cap F [s] \land int (J) (n) \cap F [s] \neq \emptyset) \to n \cap F [s] \neq \emptyset$
34	33	ex	$⊢ int (J) (n) \cap F [s] \subseteq n \cap F [s] \to (int (J) (n) \cap F [s] \neq \emptyset \to n \cap F [s] \neq \emptyset)$
35	32 34	syl	$⊢ int (J) (n) \subseteq n \to (int (J) (n) \cap F [s] \neq \emptyset \to n \cap F [s] \neq \emptyset)$
36	35	ralimdv	$⊢ int (J) (n) \subseteq n \to (\forall s \in L int (J) (n) \cap F [s] \neq \emptyset \to \forall s \in L n \cap F [s] \neq \emptyset)$
37	10 31 36	sylsyld	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land n \in nei (J) (\{A\})) \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \to \forall s \in L n \cap F [s] \neq \emptyset)$
38	37	ralrimdva	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \to \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset)$
39		simpl1	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to J \in TopOn (X)$
40	39 3	syl	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to J \in Top$
41		opnneip	$⊢ (J \in Top \land o \in J \land A \in o) \to o \in nei (J) (\{A\})$
42	41	3expb	$⊢ (J \in Top \land (o \in J \land A \in o)) \to o \in nei (J) (\{A\})$
43	40 42	sylan	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land (o \in J \land A \in o)) \to o \in nei (J) (\{A\})$
44		ineq1	$⊢ n = o \to n \cap F [s] = o \cap F [s]$
45	44	neeq1d	$⊢ n = o \to (n \cap F [s] \neq \emptyset \leftrightarrow o \cap F [s] \neq \emptyset)$
46	45	ralbidv	$⊢ n = o \to (\forall s \in L n \cap F [s] \neq \emptyset \leftrightarrow \forall s \in L o \cap F [s] \neq \emptyset)$
47	46	rspcv	$⊢ o \in nei (J) (\{A\}) \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to \forall s \in L o \cap F [s] \neq \emptyset)$
48	43 47	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land (o \in J \land A \in o)) \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to \forall s \in L o \cap F [s] \neq \emptyset)$
49	48	expr	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land o \in J) \to (A \in o \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to \forall s \in L o \cap F [s] \neq \emptyset))$
50	49	com23	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \land o \in J) \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset))$
51	50	ralrimdva	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to \forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset))$
52	38 51	impbid	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset) \leftrightarrow \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset)$
53	52	pm5.32da	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to ((A \in X \land \forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset)) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset))$
54	1 53	bitrd	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset))$

Metamath Proof Explorer

Theorem fcfnei

Proof