Step |
Hyp |
Ref |
Expression |
1 |
|
hausflf.x |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
hausflimi |
⊢ ( 𝐽 ∈ Haus → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
3 |
2
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
4 |
|
haustop |
⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top ) |
5 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
6 |
4 5
|
sylib |
⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
7 |
|
flfval |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
8 |
6 7
|
syl3an1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) |
9 |
8
|
eleq2d |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ 𝑥 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) ) |
10 |
9
|
mobidv |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃* 𝑥 𝑥 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) ) |
11 |
3 10
|
mpbird |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ∃* 𝑥 𝑥 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ) |