Metamath Proof Explorer

Theorem isflf

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

Ref Expression
Assertion isflf ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfLimfL⁡F↔A∈X∧∀o∈JA∈o→∃s∈LFs⊆o

Proof

Step Hyp Ref Expression
1 flfval ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→JfLimfL⁡F=JfLimXFilMapF⁡L
2 1 eleq2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfLimfL⁡F↔A∈JfLimXFilMapF⁡L
3 simp1 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→J∈TopOn⁡X
4 toponmax ⊢J∈TopOn⁡X→X∈J
5 4 3ad2ant1 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→X∈J
6 filfbas ⊢L∈Fil⁡Y→L∈fBas⁡Y
7 6 3ad2ant2 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→L∈fBas⁡Y
8 simp3 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→F:Y⟶X
9 fmfil ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡L∈Fil⁡X
10 5 7 8 9 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→XFilMapF⁡L∈Fil⁡X
11 flimopn ⊢J∈TopOn⁡X∧XFilMapF⁡L∈Fil⁡X→A∈JfLimXFilMapF⁡L↔A∈X∧∀o∈JA∈o→o∈XFilMapF⁡L
12 3 10 11 syl2anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfLimXFilMapF⁡L↔A∈X∧∀o∈JA∈o→o∈XFilMapF⁡L
13 toponss ⊢J∈TopOn⁡X∧o∈J→o⊆X
14 3 13 sylan ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→o⊆X
15 elfm ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X→o∈XFilMapF⁡L↔o⊆X∧∃s∈LFs⊆o
16 5 7 8 15 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→o∈XFilMapF⁡L↔o⊆X∧∃s∈LFs⊆o
17 16 adantr ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→o∈XFilMapF⁡L↔o⊆X∧∃s∈LFs⊆o
18 14 17 mpbirand ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→o∈XFilMapF⁡L↔∃s∈LFs⊆o
19 18 imbi2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→A∈o→o∈XFilMapF⁡L↔A∈o→∃s∈LFs⊆o
20 19 ralbidva ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→∀o∈JA∈o→o∈XFilMapF⁡L↔∀o∈JA∈o→∃s∈LFs⊆o
21 20 anbi2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈X∧∀o∈JA∈o→o∈XFilMapF⁡L↔A∈X∧∀o∈JA∈o→∃s∈LFs⊆o
22 2 12 21 3bitrd ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfLimfL⁡F↔A∈X∧∀o∈JA∈o→∃s∈LFs⊆o