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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
2 filtop ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌𝐿 )
3 elmapg ( ( 𝑋𝐽𝑌𝐿 ) → ( 𝐹 ∈ ( 𝑋m 𝑌 ) ↔ 𝐹 : 𝑌𝑋 ) )
4 1 2 3 syl2an ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑋m 𝑌 ) ↔ 𝐹 : 𝑌𝑋 ) )
5 4 biimpar ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ 𝐹 : 𝑌𝑋 ) → 𝐹 ∈ ( 𝑋m 𝑌 ) )
6 flffval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )
7 6 fveq1d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ‘ 𝐹 ) )
8 oveq2 ( 𝑓 = 𝐹 → ( 𝑋 FilMap 𝑓 ) = ( 𝑋 FilMap 𝐹 ) )
9 8 fveq1d ( 𝑓 = 𝐹 → ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
10 9 oveq2d ( 𝑓 = 𝐹 → ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
11 eqid ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) = ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) )
12 ovex ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ∈ V
13 10 11 12 fvmpt ( 𝐹 ∈ ( 𝑋m 𝑌 ) → ( ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
14 7 13 sylan9eq ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝑋m 𝑌 ) ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
15 5 14 syldan ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
16 15 3impa ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )