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