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 ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 simprl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
3 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → 𝑋 ∈ 𝐴 )
4 eqid ⊢ ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) )
5 4 fbasrn ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑋 ∈ 𝐴 ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
6 1 2 3 5 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
7 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → 𝐶 ∈ ( fBas ‘ 𝑌 ) )
8 eqid ⊢ ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) )
9 8 fbasrn ⊢ ( ( 𝐶 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑋 ∈ 𝐴 ) → ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
10 7 2 3 9 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
11 resmpt ⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) )
12 11 ad2antll ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) )
13 resss ⊢ ( ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ↾ 𝐵 ) ⊆ ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) )
14 12 13 eqsstrrdi ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) )
15 rnss ⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) )
16 14 15 syl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) )
17 fgss ⊢ ( ( ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) ∧ ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) ∧ ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ) → ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) ⊆ ( 𝑋 filGen ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ) )
18 6 10 16 17 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) ⊆ ( 𝑋 filGen ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ) )
19 fmval ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
20 3 1 2 19 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
21 fmval ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐶 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ) )
22 3 7 2 21 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐶 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 “ 𝑦 ) ) ) )
23 18 20 22 3sstr4d ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐵 ⊆ 𝐶 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐶 ) )