Step |
Hyp |
Ref |
Expression |
1 |
|
hausflf.x |
|- X = U. J |
2 |
|
hausflimi |
|- ( J e. Haus -> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) |
3 |
2
|
3ad2ant1 |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) |
4 |
|
haustop |
|- ( J e. Haus -> J e. Top ) |
5 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
6 |
4 5
|
sylib |
|- ( J e. Haus -> J e. ( TopOn ` X ) ) |
7 |
|
flfval |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
8 |
6 7
|
syl3an1 |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
9 |
8
|
eleq2d |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( x e. ( ( J fLimf L ) ` F ) <-> x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) ) |
10 |
9
|
mobidv |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( E* x x e. ( ( J fLimf L ) ` F ) <-> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) ) |
11 |
3 10
|
mpbird |
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) ) |