Theorem fmfnfmlem1

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

	Ref	Expression
Hypotheses	fmfnfm.b	|- ( ph -> B e. ( fBas ` Y ) )
	fmfnfm.l	|- ( ph -> L e. ( Fil ` X ) )
	fmfnfm.f	|- ( ph -> F : Y --> X )
	fmfnfm.fm	|- ( ph -> ( ( X FilMap F ) ` B ) C_ L )
Assertion	fmfnfmlem1	|- ( ph -> ( s e. ( fi ` B ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )

Proof

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 ) ) ) )