Metamath Proof Explorer

Theorem flfval

Description: Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L

Proof

Step Hyp Ref Expression
1 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
2 filtop ⊢ L ∈ Fil ⁡ Y → Y ∈ L
3 elmapg ⊢ X ∈ J ∧ Y ∈ L → F ∈ X Y ↔ F : Y ⟶ X
4 1 2 3 syl2an ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y → F ∈ X Y ↔ F : Y ⟶ X
5 4 biimpar ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → F ∈ X Y
6 flffval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y → J fLimf L = f ∈ X Y ⟼ J fLim X FilMap f ⁡ L
7 6 fveq1d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y → J fLimf L ⁡ F = f ∈ X Y ⟼ J fLim X FilMap f ⁡ L ⁡ F
8 oveq2 ⊢ f = F → X FilMap f = X FilMap F
9 8 fveq1d ⊢ f = F → X FilMap f ⁡ L = X FilMap F ⁡ L
10 9 oveq2d ⊢ f = F → J fLim X FilMap f ⁡ L = J fLim X FilMap F ⁡ L
11 eqid ⊢ f ∈ X Y ⟼ J fLim X FilMap f ⁡ L = f ∈ X Y ⟼ J fLim X FilMap f ⁡ L
12 ovex ⊢ J fLim X FilMap F ⁡ L ∈ V
13 10 11 12 fvmpt ⊢ F ∈ X Y → f ∈ X Y ⟼ J fLim X FilMap f ⁡ L ⁡ F = J fLim X FilMap F ⁡ L
14 7 13 sylan9eq ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F ∈ X Y → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
15 5 14 syldan ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
16 15 3impa ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L