Metamath Proof Explorer

Theorem fmco

Description: Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion fmco 
|- ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( X FilMap ( F o. G ) ) ` B ) = ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> B e. ( fBas ` Z ) )
2 ssfg 
 |-  ( B e. ( fBas ` Z ) -> B C_ ( Z filGen B ) )
3 1 2 syl 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> B C_ ( Z filGen B ) )
4 3 sseld 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( u e. B -> u e. ( Z filGen B ) ) )
5 simpl2 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> Y e. W )
6 simprr 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> G : Z --> Y )
7 eqid 
 |-  ( Z filGen B ) = ( Z filGen B )
8 7 imaelfm 
 |-  ( ( ( Y e. W /\ B e. ( fBas ` Z ) /\ G : Z --> Y ) /\ u e. ( Z filGen B ) ) -> ( G " u ) e. ( ( Y FilMap G ) ` B ) )
9 8 ex 
 |-  ( ( Y e. W /\ B e. ( fBas ` Z ) /\ G : Z --> Y ) -> ( u e. ( Z filGen B ) -> ( G " u ) e. ( ( Y FilMap G ) ` B ) ) )
10 5 1 6 9 syl3anc 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( u e. ( Z filGen B ) -> ( G " u ) e. ( ( Y FilMap G ) ` B ) ) )
11 4 10 syld 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( u e. B -> ( G " u ) e. ( ( Y FilMap G ) ` B ) ) )
12 11 imp 
 |-  ( ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) /\ u e. B ) -> ( G " u ) e. ( ( Y FilMap G ) ` B ) )
13 imaeq2 
 |-  ( t = ( G " u ) -> ( F " t ) = ( F " ( G " u ) ) )
14 imaco 
 |-  ( ( F o. G ) " u ) = ( F " ( G " u ) )
15 13 14 eqtr4di 
 |-  ( t = ( G " u ) -> ( F " t ) = ( ( F o. G ) " u ) )
16 15 sseq1d 
 |-  ( t = ( G " u ) -> ( ( F " t ) C_ s <-> ( ( F o. G ) " u ) C_ s ) )
17 16 rspcev 
 |-  ( ( ( G " u ) e. ( ( Y FilMap G ) ` B ) /\ ( ( F o. G ) " u ) C_ s ) -> E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s )
18 17 ex 
 |-  ( ( G " u ) e. ( ( Y FilMap G ) ` B ) -> ( ( ( F o. G ) " u ) C_ s -> E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) )
19 12 18 syl 
 |-  ( ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) /\ u e. B ) -> ( ( ( F o. G ) " u ) C_ s -> E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) )
20 19 rexlimdva 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( E. u e. B ( ( F o. G ) " u ) C_ s -> E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) )
21 elfm 
 |-  ( ( Y e. W /\ B e. ( fBas ` Z ) /\ G : Z --> Y ) -> ( t e. ( ( Y FilMap G ) ` B ) <-> ( t C_ Y /\ E. u e. B ( G " u ) C_ t ) ) )
22 5 1 6 21 syl3anc 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( t e. ( ( Y FilMap G ) ` B ) <-> ( t C_ Y /\ E. u e. B ( G " u ) C_ t ) ) )
23 sstr2 
 |-  ( ( ( F o. G ) " u ) C_ ( F " t ) -> ( ( F " t ) C_ s -> ( ( F o. G ) " u ) C_ s ) )
24 imass2 
 |-  ( ( G " u ) C_ t -> ( F " ( G " u ) ) C_ ( F " t ) )
25 14 24 eqsstrid 
 |-  ( ( G " u ) C_ t -> ( ( F o. G ) " u ) C_ ( F " t ) )
26 23 25 syl11 
 |-  ( ( F " t ) C_ s -> ( ( G " u ) C_ t -> ( ( F o. G ) " u ) C_ s ) )
27 26 reximdv 
 |-  ( ( F " t ) C_ s -> ( E. u e. B ( G " u ) C_ t -> E. u e. B ( ( F o. G ) " u ) C_ s ) )
28 27 com12 
 |-  ( E. u e. B ( G " u ) C_ t -> ( ( F " t ) C_ s -> E. u e. B ( ( F o. G ) " u ) C_ s ) )
29 28 adantl 
 |-  ( ( t C_ Y /\ E. u e. B ( G " u ) C_ t ) -> ( ( F " t ) C_ s -> E. u e. B ( ( F o. G ) " u ) C_ s ) )
30 22 29 biimtrdi 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( t e. ( ( Y FilMap G ) ` B ) -> ( ( F " t ) C_ s -> E. u e. B ( ( F o. G ) " u ) C_ s ) ) )
31 30 rexlimdv 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s -> E. u e. B ( ( F o. G ) " u ) C_ s ) )
32 20 31 impbid 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( E. u e. B ( ( F o. G ) " u ) C_ s <-> E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) )
33 32 anbi2d 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( s C_ X /\ E. u e. B ( ( F o. G ) " u ) C_ s ) <-> ( s C_ X /\ E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) ) )
34 simpl1 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> X e. V )
35 fco 
 |-  ( ( F : Y --> X /\ G : Z --> Y ) -> ( F o. G ) : Z --> X )
36 35 adantl 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( F o. G ) : Z --> X )
37 elfm 
 |-  ( ( X e. V /\ B e. ( fBas ` Z ) /\ ( F o. G ) : Z --> X ) -> ( s e. ( ( X FilMap ( F o. G ) ) ` B ) <-> ( s C_ X /\ E. u e. B ( ( F o. G ) " u ) C_ s ) ) )
38 34 1 36 37 syl3anc 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( s e. ( ( X FilMap ( F o. G ) ) ` B ) <-> ( s C_ X /\ E. u e. B ( ( F o. G ) " u ) C_ s ) ) )
39 fmfil 
 |-  ( ( Y e. W /\ B e. ( fBas ` Z ) /\ G : Z --> Y ) -> ( ( Y FilMap G ) ` B ) e. ( Fil ` Y ) )
40 5 1 6 39 syl3anc 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( Y FilMap G ) ` B ) e. ( Fil ` Y ) )
41 filfbas 
 |-  ( ( ( Y FilMap G ) ` B ) e. ( Fil ` Y ) -> ( ( Y FilMap G ) ` B ) e. ( fBas ` Y ) )
42 40 41 syl 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( Y FilMap G ) ` B ) e. ( fBas ` Y ) )
43 simprl 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> F : Y --> X )
44 elfm 
 |-  ( ( X e. V /\ ( ( Y FilMap G ) ` B ) e. ( fBas ` Y ) /\ F : Y --> X ) -> ( s e. ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) <-> ( s C_ X /\ E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) ) )
45 34 42 43 44 syl3anc 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( s e. ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) <-> ( s C_ X /\ E. t e. ( ( Y FilMap G ) ` B ) ( F " t ) C_ s ) ) )
46 33 38 45 3bitr4d 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( s e. ( ( X FilMap ( F o. G ) ) ` B ) <-> s e. ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) ) )
47 46 eqrdv 
 |-  ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( X FilMap ( F o. G ) ) ` B ) = ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) )