Metamath Proof Explorer

Theorem fmfnfm

Description: A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-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 fmfnfm 
|- ( ph -> E. f e. ( Fil ` Y ) ( B C_ f /\ L = ( ( X FilMap F ) ` f ) ) )

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 fbsspw 
 |-  ( B e. ( fBas ` Y ) -> B C_ ~P Y )
6 1 5 syl 
 |-  ( ph -> B C_ ~P Y )
7 elfvdm 
 |-  ( B e. ( fBas ` Y ) -> Y e. dom fBas )
8 1 7 syl 
 |-  ( ph -> Y e. dom fBas )
9 ffn 
 |-  ( F : Y --> X -> F Fn Y )
10 dffn4 
 |-  ( F Fn Y <-> F : Y -onto-> ran F )
11 9 10 sylib 
 |-  ( F : Y --> X -> F : Y -onto-> ran F )
12 foima 
 |-  ( F : Y -onto-> ran F -> ( F " Y ) = ran F )
13 3 11 12 3syl 
 |-  ( ph -> ( F " Y ) = ran F )
14 filtop 
 |-  ( L e. ( Fil ` X ) -> X e. L )
15 2 14 syl 
 |-  ( ph -> X e. L )
16 fgcl 
 |-  ( B e. ( fBas ` Y ) -> ( Y filGen B ) e. ( Fil ` Y ) )
17 filtop 
 |-  ( ( Y filGen B ) e. ( Fil ` Y ) -> Y e. ( Y filGen B ) )
18 1 16 17 3syl 
 |-  ( ph -> Y e. ( Y filGen B ) )
19 eqid 
 |-  ( Y filGen B ) = ( Y filGen B )
20 19 imaelfm 
 |-  ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ Y e. ( Y filGen B ) ) -> ( F " Y ) e. ( ( X FilMap F ) ` B ) )
21 15 1 3 18 20 syl31anc 
 |-  ( ph -> ( F " Y ) e. ( ( X FilMap F ) ` B ) )
22 13 21 eqeltrrd 
 |-  ( ph -> ran F e. ( ( X FilMap F ) ` B ) )
23 4 22 sseldd 
 |-  ( ph -> ran F e. L )
24 rnelfmlem 
 |-  ( ( ( Y e. dom fBas /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )
25 8 2 3 23 24 syl31anc 
 |-  ( ph -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )
26 fbsspw 
 |-  ( ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) -> ran ( x e. L |-> ( `' F " x ) ) C_ ~P Y )
27 25 26 syl 
 |-  ( ph -> ran ( x e. L |-> ( `' F " x ) ) C_ ~P Y )
28 6 27 unssd 
 |-  ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ~P Y )
29 ssun1 
 |-  B C_ ( B u. ran ( x e. L |-> ( `' F " x ) ) )
30 fbasne0 
 |-  ( B e. ( fBas ` Y ) -> B =/= (/) )
31 1 30 syl 
 |-  ( ph -> B =/= (/) )
32 ssn0 
 |-  ( ( B C_ ( B u. ran ( x e. L |-> ( `' F " x ) ) ) /\ B =/= (/) ) -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) =/= (/) )
33 29 31 32 sylancr 
 |-  ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) =/= (/) )
34 eqid 
 |-  ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
35 34 elrnmpt 
 |-  ( t e. _V -> ( t e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L t = ( `' F " x ) ) )
36 35 elv 
 |-  ( t e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L t = ( `' F " x ) )
37 0nelfil 
 |-  ( L e. ( Fil ` X ) -> -. (/) e. L )
38 2 37 syl 
 |-  ( ph -> -. (/) e. L )
39 38 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> -. (/) e. L )
40 2 adantr 
 |-  ( ( ph /\ s e. B ) -> L e. ( Fil ` X ) )
41 4 adantr 
 |-  ( ( ph /\ s e. B ) -> ( ( X FilMap F ) ` B ) C_ L )
42 15 1 3 3jca 
 |-  ( ph -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
43 42 adantr 
 |-  ( ( ph /\ s e. B ) -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
44 ssfg 
 |-  ( B e. ( fBas ` Y ) -> B C_ ( Y filGen B ) )
45 1 44 syl 
 |-  ( ph -> B C_ ( Y filGen B ) )
46 45 sselda 
 |-  ( ( ph /\ s e. B ) -> s e. ( Y filGen B ) )
47 19 imaelfm 
 |-  ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ s e. ( Y filGen B ) ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
48 43 46 47 syl2anc 
 |-  ( ( ph /\ s e. B ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
49 41 48 sseldd 
 |-  ( ( ph /\ s e. B ) -> ( F " s ) e. L )
50 40 49 jca 
 |-  ( ( ph /\ s e. B ) -> ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) )
51 filin 
 |-  ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
52 51 3expa 
 |-  ( ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
53 50 52 sylan 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
54 eleq1 
 |-  ( ( ( F " s ) i^i x ) = (/) -> ( ( ( F " s ) i^i x ) e. L <-> (/) e. L ) )
55 53 54 syl5ibcom 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( ( ( F " s ) i^i x ) = (/) -> (/) e. L ) )
56 39 55 mtod 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> -. ( ( F " s ) i^i x ) = (/) )
57 neq0 
 |-  ( -. ( ( F " s ) i^i x ) = (/) <-> E. t t e. ( ( F " s ) i^i x ) )
58 elin 
 |-  ( t e. ( ( F " s ) i^i x ) <-> ( t e. ( F " s ) /\ t e. x ) )
59 ffun 
 |-  ( F : Y --> X -> Fun F )
60 fvelima 
 |-  ( ( Fun F /\ t e. ( F " s ) ) -> E. y e. s ( F ` y ) = t )
61 60 ex 
 |-  ( Fun F -> ( t e. ( F " s ) -> E. y e. s ( F ` y ) = t ) )
62 3 59 61 3syl 
 |-  ( ph -> ( t e. ( F " s ) -> E. y e. s ( F ` y ) = t ) )
63 62 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( t e. ( F " s ) -> E. y e. s ( F ` y ) = t ) )
64 3 59 syl 
 |-  ( ph -> Fun F )
65 64 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> Fun F )
66 fbelss 
 |-  ( ( B e. ( fBas ` Y ) /\ s e. B ) -> s C_ Y )
67 1 66 sylan 
 |-  ( ( ph /\ s e. B ) -> s C_ Y )
68 3 fdmd 
 |-  ( ph -> dom F = Y )
69 68 adantr 
 |-  ( ( ph /\ s e. B ) -> dom F = Y )
70 67 69 sseqtrrd 
 |-  ( ( ph /\ s e. B ) -> s C_ dom F )
71 70 adantr 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> s C_ dom F )
72 71 sselda 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> y e. dom F )
73 fvimacnv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
74 65 72 73 syl2anc 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
75 inelcm 
 |-  ( ( y e. s /\ y e. ( `' F " x ) ) -> ( s i^i ( `' F " x ) ) =/= (/) )
76 75 ex 
 |-  ( y e. s -> ( y e. ( `' F " x ) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
77 76 adantl 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> ( y e. ( `' F " x ) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
78 74 77 sylbid 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> ( ( F ` y ) e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) )
79 eleq1 
 |-  ( ( F ` y ) = t -> ( ( F ` y ) e. x <-> t e. x ) )
80 79 imbi1d 
 |-  ( ( F ` y ) = t -> ( ( ( F ` y ) e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) <-> ( t e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) ) )
81 78 80 syl5ibcom 
 |-  ( ( ( ( ph /\ s e. B ) /\ x e. L ) /\ y e. s ) -> ( ( F ` y ) = t -> ( t e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) ) )
82 81 rexlimdva 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( E. y e. s ( F ` y ) = t -> ( t e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) ) )
83 63 82 syld 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( t e. ( F " s ) -> ( t e. x -> ( s i^i ( `' F " x ) ) =/= (/) ) ) )
84 83 impd 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( ( t e. ( F " s ) /\ t e. x ) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
85 58 84 biimtrid 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( t e. ( ( F " s ) i^i x ) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
86 85 exlimdv 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( E. t t e. ( ( F " s ) i^i x ) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
87 57 86 biimtrid 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( -. ( ( F " s ) i^i x ) = (/) -> ( s i^i ( `' F " x ) ) =/= (/) ) )
88 56 87 mpd 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( s i^i ( `' F " x ) ) =/= (/) )
89 ineq2 
 |-  ( t = ( `' F " x ) -> ( s i^i t ) = ( s i^i ( `' F " x ) ) )
90 89 neeq1d 
 |-  ( t = ( `' F " x ) -> ( ( s i^i t ) =/= (/) <-> ( s i^i ( `' F " x ) ) =/= (/) ) )
91 88 90 syl5ibrcom 
 |-  ( ( ( ph /\ s e. B ) /\ x e. L ) -> ( t = ( `' F " x ) -> ( s i^i t ) =/= (/) ) )
92 91 rexlimdva 
 |-  ( ( ph /\ s e. B ) -> ( E. x e. L t = ( `' F " x ) -> ( s i^i t ) =/= (/) ) )
93 36 92 biimtrid 
 |-  ( ( ph /\ s e. B ) -> ( t e. ran ( x e. L |-> ( `' F " x ) ) -> ( s i^i t ) =/= (/) ) )
94 93 expimpd 
 |-  ( ph -> ( ( s e. B /\ t e. ran ( x e. L |-> ( `' F " x ) ) ) -> ( s i^i t ) =/= (/) ) )
95 94 ralrimivv 
 |-  ( ph -> A. s e. B A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) =/= (/) )
96 fbunfip 
 |-  ( ( B e. ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) <-> A. s e. B A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) =/= (/) ) )
97 1 25 96 syl2anc 
 |-  ( ph -> ( -. (/) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) <-> A. s e. B A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) =/= (/) ) )
98 95 97 mpbird 
 |-  ( ph -> -. (/) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
99 fsubbas 
 |-  ( Y e. dom fBas -> ( ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) <-> ( ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ~P Y /\ ( B u. ran ( x e. L |-> ( `' F " x ) ) ) =/= (/) /\ -. (/) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
100 1 7 99 3syl 
 |-  ( ph -> ( ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) <-> ( ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ~P Y /\ ( B u. ran ( x e. L |-> ( `' F " x ) ) ) =/= (/) /\ -. (/) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
101 28 33 98 100 mpbir3and 
 |-  ( ph -> ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) )
102 fgcl 
 |-  ( ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) -> ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) e. ( Fil ` Y ) )
103 101 102 syl 
 |-  ( ph -> ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) e. ( Fil ` Y ) )
104 unexg 
 |-  ( ( B e. ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) ) -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
105 1 25 104 syl2anc 
 |-  ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
106 ssfii 
 |-  ( ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
107 105 106 syl 
 |-  ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
108 107 unssad 
 |-  ( ph -> B C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
109 ssfg 
 |-  ( ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) -> ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) )
110 101 109 syl 
 |-  ( ph -> ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) )
111 108 110 sstrd 
 |-  ( ph -> B C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) )
112 1 2 3 4 fmfnfmlem4 
 |-  ( ph -> ( t e. L <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
113 elfm 
 |-  ( ( X e. L /\ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) /\ F : Y --> X ) -> ( t e. ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
114 15 101 3 113 syl3anc 
 |-  ( ph -> ( t e. ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
115 112 114 bitr4d 
 |-  ( ph -> ( t e. L <-> t e. ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
116 115 eqrdv 
 |-  ( ph -> L = ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) )
117 eqid 
 |-  ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) = ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
118 117 fmfg 
 |-  ( ( X e. L /\ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
119 15 101 3 118 syl3anc 
 |-  ( ph -> ( ( X FilMap F ) ` ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
120 116 119 eqtrd 
 |-  ( ph -> L = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
121 sseq2 
 |-  ( f = ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( B C_ f <-> B C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
122 fveq2 
 |-  ( f = ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( ( X FilMap F ) ` f ) = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) )
123 122 eqeq2d 
 |-  ( f = ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( L = ( ( X FilMap F ) ` f ) <-> L = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) ) )
124 121 123 anbi12d 
 |-  ( f = ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( ( B C_ f /\ L = ( ( X FilMap F ) ` f ) ) <-> ( B C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) /\ L = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) ) ) )
125 124 rspcev 
 |-  ( ( ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) e. ( Fil ` Y ) /\ ( B C_ ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) /\ L = ( ( X FilMap F ) ` ( Y filGen ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ) ) ) ) -> E. f e. ( Fil ` Y ) ( B C_ f /\ L = ( ( X FilMap F ) ` f ) ) )
126 103 111 120 125 syl12anc 
 |-  ( ph -> E. f e. ( Fil ` Y ) ( B C_ f /\ L = ( ( X FilMap F ) ` f ) ) )