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 𝑓 ) ‘ 𝐿 ) ) ) )