Theorem fmfg

Description: The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

	Ref	Expression
Hypothesis	elfm2.l	|- L = ( Y filGen B )
Assertion	fmfg	|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( ( X FilMap F ) ` L ) )

Proof

Step	Hyp	Ref	Expression
1		elfm2.l	|- L = ( Y filGen B )
2	1	elfm2	|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` B ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
3		fgcl	|- ( B e. ( fBas ` Y ) -> ( Y filGen B ) e. ( Fil ` Y ) )
4	1 3	eqeltrid	|- ( B e. ( fBas ` Y ) -> L e. ( Fil ` Y ) )
5		filfbas	|- ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) )
6	4 5	syl	|- ( B e. ( fBas ` Y ) -> L e. ( fBas ` Y ) )
7		elfm	|- ( ( X e. C /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` L ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
8	6 7	syl3an2	|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` L ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
9	2 8	bitr4d	|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` B ) <-> x e. ( ( X FilMap F ) ` L ) ) )
10	9	eqrdv	|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( ( X FilMap F ) ` L ) )