Step |
Hyp |
Ref |
Expression |
1 |
|
hausflf.x |
|- X = U. J |
2 |
|
n0 |
|- ( ( ( J fLimf L ) ` F ) =/= (/) <-> E. x x e. ( ( J fLimf L ) ` F ) ) |
3 |
2
|
biimpi |
|- ( ( ( J fLimf L ) ` F ) =/= (/) -> E. x x e. ( ( J fLimf L ) ` F ) ) |
4 |
1
|
hausflf |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) ) |
5 |
|
euen1b |
|- ( ( ( J fLimf L ) ` F ) ~~ 1o <-> E! x x e. ( ( J fLimf L ) ` F ) ) |
6 |
|
df-eu |
|- ( E! x x e. ( ( J fLimf L ) ` F ) <-> ( E. x x e. ( ( J fLimf L ) ` F ) /\ E* x x e. ( ( J fLimf L ) ` F ) ) ) |
7 |
5 6
|
sylbbr |
|- ( ( E. x x e. ( ( J fLimf L ) ` F ) /\ E* x x e. ( ( J fLimf L ) ` F ) ) -> ( ( J fLimf L ) ` F ) ~~ 1o ) |
8 |
3 4 7
|
syl2anr |
|- ( ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( ( J fLimf L ) ` F ) =/= (/) ) -> ( ( J fLimf L ) ` F ) ~~ 1o ) |