Step |
Hyp |
Ref |
Expression |
1 |
|
flimfcls |
|- ( J fLim ( ( X FilMap F ) ` L ) ) C_ ( J fClus ( ( X FilMap F ) ` L ) ) |
2 |
1
|
a1i |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( J fLim ( ( X FilMap F ) ` L ) ) C_ ( J fClus ( ( X FilMap F ) ` L ) ) ) |
3 |
|
flfval |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
4 |
|
fcfval |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) ) |
5 |
2 3 4
|
3sstr4d |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) C_ ( ( J fClusf L ) ` F ) ) |