Metamath Proof Explorer


Theorem flffval

Description: Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009) (Revised by Mario Carneiro, 15-Dec-2013) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flffval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )

Proof

Step Hyp Ref Expression
1 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 fvssunirn ( Fil ‘ 𝑌 ) ⊆ ran Fil
3 2 sseli ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ran Fil )
4 unieq ( 𝑥 = 𝐽 𝑥 = 𝐽 )
5 unieq ( 𝑦 = 𝐿 𝑦 = 𝐿 )
6 4 5 oveqan12d ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → ( 𝑥m 𝑦 ) = ( 𝐽m 𝐿 ) )
7 simpl ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → 𝑥 = 𝐽 )
8 4 adantr ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → 𝑥 = 𝐽 )
9 8 oveq1d ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → ( 𝑥 FilMap 𝑓 ) = ( 𝐽 FilMap 𝑓 ) )
10 simpr ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → 𝑦 = 𝐿 )
11 9 10 fveq12d ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) = ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) )
12 7 11 oveq12d ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → ( 𝑥 fLim ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) = ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) )
13 6 12 mpteq12dv ( ( 𝑥 = 𝐽𝑦 = 𝐿 ) → ( 𝑓 ∈ ( 𝑥m 𝑦 ) ↦ ( 𝑥 fLim ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) = ( 𝑓 ∈ ( 𝐽m 𝐿 ) ↦ ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )
14 df-flf fLimf = ( 𝑥 ∈ Top , 𝑦 ran Fil ↦ ( 𝑓 ∈ ( 𝑥m 𝑦 ) ↦ ( 𝑥 fLim ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) )
15 ovex ( 𝐽m 𝐿 ) ∈ V
16 15 mptex ( 𝑓 ∈ ( 𝐽m 𝐿 ) ↦ ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ∈ V
17 13 14 16 ovmpoa ( ( 𝐽 ∈ Top ∧ 𝐿 ran Fil ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝐽m 𝐿 ) ↦ ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )
18 1 3 17 syl2an ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝐽m 𝐿 ) ↦ ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )
19 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
20 19 eqcomd ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 = 𝑋 )
21 filunibas ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 = 𝑌 )
22 20 21 oveqan12d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽m 𝐿 ) = ( 𝑋m 𝑌 ) )
23 20 adantr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → 𝐽 = 𝑋 )
24 23 oveq1d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 FilMap 𝑓 ) = ( 𝑋 FilMap 𝑓 ) )
25 24 fveq1d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) = ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) )
26 25 oveq2d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) )
27 22 26 mpteq12dv ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝐽m 𝐿 ) ↦ ( 𝐽 fLim ( ( 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) = ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )
28 18 27 eqtrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝑋m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) )