Theorem funimass1

Description: A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004)

	Ref	Expression
Assertion	funimass1	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 → 𝐴 ⊆ ( 𝐹 “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imass2	⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐵 ) )
2		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) = ( 𝐴 ∩ ran 𝐹 ) )
3		dfss	⊢ ( 𝐴 ⊆ ran 𝐹 ↔ 𝐴 = ( 𝐴 ∩ ran 𝐹 ) )
4	3	biimpi	⊢ ( 𝐴 ⊆ ran 𝐹 → 𝐴 = ( 𝐴 ∩ ran 𝐹 ) )
5	4	eqcomd	⊢ ( 𝐴 ⊆ ran 𝐹 → ( 𝐴 ∩ ran 𝐹 ) = 𝐴 )
6	2 5	sylan9eq	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) = 𝐴 )
7	6	sseq1d	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐵 ) ↔ 𝐴 ⊆ ( 𝐹 “ 𝐵 ) ) )
8	1 7	imbitrid	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 → 𝐴 ⊆ ( 𝐹 “ 𝐵 ) ) )