isfcf

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

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		fcfval	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = J fClus (X FilMap F) (L)$
2	1	eleq2d	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \leftrightarrow A \in (J fClus (X FilMap F) (L)))$
3		simp1	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to J \in TopOn (X)$
4		toponmax	$⊢ J \in TopOn (X) \to X \in J$
5		filfbas	$⊢ L \in Fil (Y) \to L \in fBas (Y)$
6		id	$⊢ F : Y ⟶ X \to F : Y ⟶ X$
7		fmfil	$⊢ (X \in J \land L \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
8	4 5 6 7	syl3an	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
9		fclsopn	$⊢ (J \in TopOn (X) \land (X FilMap F) (L) \in Fil (X)) \to (A \in (J fClus (X FilMap F) (L)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall x \in (X FilMap F) (L) o \cap x \neq \emptyset)))$
10	3 8 9	syl2anc	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClus (X FilMap F) (L)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall x \in (X FilMap F) (L) o \cap x \neq \emptyset)))$
11		simpll1	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to J \in TopOn (X)$
12	11 4	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to X \in J$
13		simpll2	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to L \in Fil (Y)$
14	13 5	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to L \in fBas (Y)$
15		simpll3	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to F : Y ⟶ X$
16		simpl2	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to L \in Fil (Y)$
17		fgfil	$⊢ L \in Fil (Y) \to Y filGen L = L$
18	16 17	syl	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to Y filGen L = L$
19	18	eleq2d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to (s \in (Y filGen L) \leftrightarrow s \in L)$
20	19	biimpar	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to s \in (Y filGen L)$
21		eqid	$⊢ Y filGen L = Y filGen L$
22	21	imaelfm	$⊢ ((X \in J \land L \in fBas (Y) \land F : Y ⟶ X) \land s \in (Y filGen L)) \to F [s] \in (X FilMap F) (L)$
23	12 14 15 20 22	syl31anc	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to F [s] \in (X FilMap F) (L)$
24		ineq2	$⊢ x = F [s] \to o \cap x = o \cap F [s]$
25	24	neeq1d	$⊢ x = F [s] \to (o \cap x \neq \emptyset \leftrightarrow o \cap F [s] \neq \emptyset)$
26	25	rspcv	$⊢ F [s] \in (X FilMap F) (L) \to (\forall x \in (X FilMap F) (L) o \cap x \neq \emptyset \to o \cap F [s] \neq \emptyset)$
27	23 26	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land s \in L) \to (\forall x \in (X FilMap F) (L) o \cap x \neq \emptyset \to o \cap F [s] \neq \emptyset)$
28	27	ralrimdva	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to (\forall x \in (X FilMap F) (L) o \cap x \neq \emptyset \to \forall s \in L o \cap F [s] \neq \emptyset)$
29		elfm	$⊢ (X \in J \land L \in fBas (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (L) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
30	4 5 6 29	syl3an	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (L) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
31	30	adantr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to (x \in (X FilMap F) (L) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
32	31	simplbda	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land x \in (X FilMap F) (L)) \to \exists s \in L F [s] \subseteq x$
33		r19.29r	$⊢ (\exists s \in L F [s] \subseteq x \land \forall s \in L o \cap F [s] \neq \emptyset) \to \exists s \in L (F [s] \subseteq x \land o \cap F [s] \neq \emptyset)$
34		sslin	$⊢ F [s] \subseteq x \to o \cap F [s] \subseteq o \cap x$
35		ssn0	$⊢ (o \cap F [s] \subseteq o \cap x \land o \cap F [s] \neq \emptyset) \to o \cap x \neq \emptyset$
36	34 35	sylan	$⊢ (F [s] \subseteq x \land o \cap F [s] \neq \emptyset) \to o \cap x \neq \emptyset$
37	36	rexlimivw	$⊢ \exists s \in L (F [s] \subseteq x \land o \cap F [s] \neq \emptyset) \to o \cap x \neq \emptyset$
38	33 37	syl	$⊢ (\exists s \in L F [s] \subseteq x \land \forall s \in L o \cap F [s] \neq \emptyset) \to o \cap x \neq \emptyset$
39	38	ex	$⊢ \exists s \in L F [s] \subseteq x \to (\forall s \in L o \cap F [s] \neq \emptyset \to o \cap x \neq \emptyset)$
40	32 39	syl	$⊢ (((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \land x \in (X FilMap F) (L)) \to (\forall s \in L o \cap F [s] \neq \emptyset \to o \cap x \neq \emptyset)$
41	40	ralrimdva	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to (\forall s \in L o \cap F [s] \neq \emptyset \to \forall x \in (X FilMap F) (L) o \cap x \neq \emptyset)$
42	28 41	impbid	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to (\forall x \in (X FilMap F) (L) o \cap x \neq \emptyset \leftrightarrow \forall s \in L o \cap F [s] \neq \emptyset)$
43	42	imbi2d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land o \in J) \to ((A \in o \to \forall x \in (X FilMap F) (L) o \cap x \neq \emptyset) \leftrightarrow (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset))$
44	43	ralbidva	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (\forall o \in J (A \in o \to \forall x \in (X FilMap F) (L) o \cap x \neq \emptyset) \leftrightarrow \forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset))$
45	44	anbi2d	$⊢ (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 x \in (X FilMap F) (L) o \cap x \neq \emptyset)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in L o \cap F [s] \neq \emptyset)))$
46	2 10 45	3bitrd	$⊢ (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)))$

Metamath Proof Explorer

Theorem isfcf

Proof