Step |
Hyp |
Ref |
Expression |
1 |
|
toponmax |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 ) |
2 |
|
fmufil |
⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) ) |
3 |
1 2
|
syl3an1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) ) |
4 |
|
uffclsflim |
⊢ ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
6 |
|
ufilfil |
⊢ ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) ) |
7 |
|
fcfval |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
8 |
6 7
|
syl3an2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
9 |
|
flfval |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
10 |
6 9
|
syl3an2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
11 |
5 8 10
|
3eqtr4d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ) |