flfnei

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

		Ref	Expression
	Assertion	flfnei	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n))$

Proof

Step	Hyp	Ref	Expression
1		flfval	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$
2	1	eleq2d	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow A \in (J fLim (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	4	3ad2ant1	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to X \in J$
6		filfbas	$⊢ L \in Fil (Y) \to L \in fBas (Y)$
7	6	3ad2ant2	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to L \in fBas (Y)$
8		simp3	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to F : Y ⟶ X$
9		fmfil	$⊢ (X \in J \land L \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
10	5 7 8 9	syl3anc	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
11		elflim	$⊢ (J \in TopOn (X) \land (X FilMap F) (L) \in Fil (X)) \to (A \in (J fLim (X FilMap F) (L)) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq (X FilMap F) (L)))$
12	3 10 11	syl2anc	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLim (X FilMap F) (L)) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq (X FilMap F) (L)))$
13		dfss3	$⊢ nei (J) (\{A\}) \subseteq (X FilMap F) (L) \leftrightarrow \forall n \in nei (J) (\{A\}) n \in (X FilMap F) (L)$
14		topontop	$⊢ J \in TopOn (X) \to J \in Top$
15	14	3ad2ant1	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to J \in Top$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	neii1	$⊢ (J \in Top \land n \in nei (J) (\{A\})) \to n \subseteq ⋃ J$
18	15 17	sylan	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land n \in nei (J) (\{A\})) \to n \subseteq ⋃ J$
19		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
20	19	3ad2ant1	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to X = ⋃ J$
21	20	adantr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land n \in nei (J) (\{A\})) \to X = ⋃ J$
22	18 21	sseqtrrd	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land n \in nei (J) (\{A\})) \to n \subseteq X$
23		elfm	$⊢ (X \in J \land L \in fBas (Y) \land F : Y ⟶ X) \to (n \in (X FilMap F) (L) \leftrightarrow (n \subseteq X \land \exists s \in L F [s] \subseteq n))$
24	5 7 8 23	syl3anc	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (n \in (X FilMap F) (L) \leftrightarrow (n \subseteq X \land \exists s \in L F [s] \subseteq n))$
25	24	baibd	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land n \subseteq X) \to (n \in (X FilMap F) (L) \leftrightarrow \exists s \in L F [s] \subseteq n)$
26	22 25	syldan	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land n \in nei (J) (\{A\})) \to (n \in (X FilMap F) (L) \leftrightarrow \exists s \in L F [s] \subseteq n)$
27	26	ralbidva	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (\forall n \in nei (J) (\{A\}) n \in (X FilMap F) (L) \leftrightarrow \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n)$
28	13 27	bitrid	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (nei (J) (\{A\}) \subseteq (X FilMap F) (L) \leftrightarrow \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n)$
29	28	anbi2d	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to ((A \in X \land nei (J) (\{A\}) \subseteq (X FilMap F) (L)) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n))$
30	2 12 29	3bitrd	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n))$

Metamath Proof Explorer

Theorem flfnei

Proof