| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fmfnfm.b |
|- ( ph -> B e. ( fBas ` Y ) ) |
| 2 |
|
fmfnfm.l |
|- ( ph -> L e. ( Fil ` X ) ) |
| 3 |
|
fmfnfm.f |
|- ( ph -> F : Y --> X ) |
| 4 |
|
fmfnfm.fm |
|- ( ph -> ( ( X FilMap F ) ` B ) C_ L ) |
| 5 |
|
fbssfi |
|- ( ( B e. ( fBas ` Y ) /\ s e. ( fi ` B ) ) -> E. w e. B w C_ s ) |
| 6 |
1 5
|
sylan |
|- ( ( ph /\ s e. ( fi ` B ) ) -> E. w e. B w C_ s ) |
| 7 |
|
sstr2 |
|- ( ( F " w ) C_ ( F " s ) -> ( ( F " s ) C_ t -> ( F " w ) C_ t ) ) |
| 8 |
|
imass2 |
|- ( w C_ s -> ( F " w ) C_ ( F " s ) ) |
| 9 |
7 8
|
syl11 |
|- ( ( F " s ) C_ t -> ( w C_ s -> ( F " w ) C_ t ) ) |
| 10 |
9
|
reximdv |
|- ( ( F " s ) C_ t -> ( E. w e. B w C_ s -> E. w e. B ( F " w ) C_ t ) ) |
| 11 |
6 10
|
syl5com |
|- ( ( ph /\ s e. ( fi ` B ) ) -> ( ( F " s ) C_ t -> E. w e. B ( F " w ) C_ t ) ) |
| 12 |
|
filtop |
|- ( L e. ( Fil ` X ) -> X e. L ) |
| 13 |
2 12
|
syl |
|- ( ph -> X e. L ) |
| 14 |
|
elfm |
|- ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( t e. ( ( X FilMap F ) ` B ) <-> ( t C_ X /\ E. w e. B ( F " w ) C_ t ) ) ) |
| 15 |
13 1 3 14
|
syl3anc |
|- ( ph -> ( t e. ( ( X FilMap F ) ` B ) <-> ( t C_ X /\ E. w e. B ( F " w ) C_ t ) ) ) |
| 16 |
4
|
sseld |
|- ( ph -> ( t e. ( ( X FilMap F ) ` B ) -> t e. L ) ) |
| 17 |
15 16
|
sylbird |
|- ( ph -> ( ( t C_ X /\ E. w e. B ( F " w ) C_ t ) -> t e. L ) ) |
| 18 |
17
|
expcomd |
|- ( ph -> ( E. w e. B ( F " w ) C_ t -> ( t C_ X -> t e. L ) ) ) |
| 19 |
18
|
adantr |
|- ( ( ph /\ s e. ( fi ` B ) ) -> ( E. w e. B ( F " w ) C_ t -> ( t C_ X -> t e. L ) ) ) |
| 20 |
11 19
|
syld |
|- ( ( ph /\ s e. ( fi ` B ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) |
| 21 |
20
|
ex |
|- ( ph -> ( s e. ( fi ` B ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) ) |