# Metamath Proof Explorer

## Theorem sspreima

Description: The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017)

Ref Expression
Assertion sspreima ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq {B}\right)\to {{F}}^{-1}\left[{A}\right]\subseteq {{F}}^{-1}\left[{B}\right]$

### Proof

Step Hyp Ref Expression
1 inpreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\cap {B}\right]={{F}}^{-1}\left[{A}\right]\cap {{F}}^{-1}\left[{B}\right]$
2 df-ss ${⊢}{A}\subseteq {B}↔{A}\cap {B}={A}$
3 2 biimpi ${⊢}{A}\subseteq {B}\to {A}\cap {B}={A}$
4 3 imaeq2d ${⊢}{A}\subseteq {B}\to {{F}}^{-1}\left[{A}\cap {B}\right]={{F}}^{-1}\left[{A}\right]$
5 1 4 sylan9req ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq {B}\right)\to {{F}}^{-1}\left[{A}\right]\cap {{F}}^{-1}\left[{B}\right]={{F}}^{-1}\left[{A}\right]$
6 df-ss ${⊢}{{F}}^{-1}\left[{A}\right]\subseteq {{F}}^{-1}\left[{B}\right]↔{{F}}^{-1}\left[{A}\right]\cap {{F}}^{-1}\left[{B}\right]={{F}}^{-1}\left[{A}\right]$
7 5 6 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq {B}\right)\to {{F}}^{-1}\left[{A}\right]\subseteq {{F}}^{-1}\left[{B}\right]$