Metamath Proof Explorer

Theorem fmss

Description: A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion fmss ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→XFilMapF⁡B⊆XFilMapF⁡C

Proof

Step Hyp Ref Expression
1 simpl2 ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→B∈fBas⁡Y
2 simprl ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→F:Y⟶X
3 simpl1 ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→X∈A
4 eqid ⊢ran⁡y∈B⟼Fy=ran⁡y∈B⟼Fy
5 4 fbasrn ⊢B∈fBas⁡Y∧F:Y⟶X∧X∈A→ran⁡y∈B⟼Fy∈fBas⁡X
6 1 2 3 5 syl3anc ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→ran⁡y∈B⟼Fy∈fBas⁡X
7 simpl3 ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→C∈fBas⁡Y
8 eqid ⊢ran⁡y∈C⟼Fy=ran⁡y∈C⟼Fy
9 8 fbasrn ⊢C∈fBas⁡Y∧F:Y⟶X∧X∈A→ran⁡y∈C⟼Fy∈fBas⁡X
10 7 2 3 9 syl3anc ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→ran⁡y∈C⟼Fy∈fBas⁡X
11 resmpt ⊢B⊆C→y∈C⟼Fy↾B=y∈B⟼Fy
12 11 ad2antll ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→y∈C⟼Fy↾B=y∈B⟼Fy
13 resss ⊢y∈C⟼Fy↾B⊆y∈C⟼Fy
14 12 13 eqsstrrdi ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→y∈B⟼Fy⊆y∈C⟼Fy
15 rnss ⊢y∈B⟼Fy⊆y∈C⟼Fy→ran⁡y∈B⟼Fy⊆ran⁡y∈C⟼Fy
16 14 15 syl ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→ran⁡y∈B⟼Fy⊆ran⁡y∈C⟼Fy
17 fgss ⊢ran⁡y∈B⟼Fy∈fBas⁡X∧ran⁡y∈C⟼Fy∈fBas⁡X∧ran⁡y∈B⟼Fy⊆ran⁡y∈C⟼Fy→XfilGenran⁡y∈B⟼Fy⊆XfilGenran⁡y∈C⟼Fy
18 6 10 16 17 syl3anc ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→XfilGenran⁡y∈B⟼Fy⊆XfilGenran⁡y∈C⟼Fy
19 fmval ⊢X∈A∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B=XfilGenran⁡y∈B⟼Fy
20 3 1 2 19 syl3anc ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→XFilMapF⁡B=XfilGenran⁡y∈B⟼Fy
21 fmval ⊢X∈A∧C∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡C=XfilGenran⁡y∈C⟼Fy
22 3 7 2 21 syl3anc ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→XFilMapF⁡C=XfilGenran⁡y∈C⟼Fy
23 18 20 22 3sstr4d ⊢X∈A∧B∈fBas⁡Y∧C∈fBas⁡Y∧F:Y⟶X∧B⊆C→XFilMapF⁡B⊆XFilMapF⁡C