Description: The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | resimass | ⊢ ( ( 𝐴 ↾ 𝐵 ) “ 𝐶 ) ⊆ ( 𝐴 “ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resss | ⊢ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴 | |
2 | imass1 | ⊢ ( ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴 → ( ( 𝐴 ↾ 𝐵 ) “ 𝐶 ) ⊆ ( 𝐴 “ 𝐶 ) ) | |
3 | 1 2 | ax-mp | ⊢ ( ( 𝐴 ↾ 𝐵 ) “ 𝐶 ) ⊆ ( 𝐴 “ 𝐶 ) |