Metamath Proof Explorer


Theorem imadifss

Description: The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Assertion imadifss ( ( 𝐹𝐴 ) ∖ ( 𝐹𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssun2 𝐴 ⊆ ( 𝐵𝐴 )
2 undif2 ( 𝐵 ∪ ( 𝐴𝐵 ) ) = ( 𝐵𝐴 )
3 1 2 sseqtrri 𝐴 ⊆ ( 𝐵 ∪ ( 𝐴𝐵 ) )
4 imass2 ( 𝐴 ⊆ ( 𝐵 ∪ ( 𝐴𝐵 ) ) → ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ( 𝐵 ∪ ( 𝐴𝐵 ) ) ) )
5 3 4 ax-mp ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ( 𝐵 ∪ ( 𝐴𝐵 ) ) )
6 imaundi ( 𝐹 “ ( 𝐵 ∪ ( 𝐴𝐵 ) ) ) = ( ( 𝐹𝐵 ) ∪ ( 𝐹 “ ( 𝐴𝐵 ) ) )
7 5 6 sseqtri ( 𝐹𝐴 ) ⊆ ( ( 𝐹𝐵 ) ∪ ( 𝐹 “ ( 𝐴𝐵 ) ) )
8 ssundif ( ( 𝐹𝐴 ) ⊆ ( ( 𝐹𝐵 ) ∪ ( 𝐹 “ ( 𝐴𝐵 ) ) ) ↔ ( ( 𝐹𝐴 ) ∖ ( 𝐹𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴𝐵 ) ) )
9 7 8 mpbi ( ( 𝐹𝐴 ) ∖ ( 𝐹𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴𝐵 ) )