Theorem funimass2

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

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

Proof

Step	Hyp	Ref	Expression
1		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) = ( 𝐵 ∩ ran 𝐹 ) )
2	1	sseq2d	⊢ ( Fun 𝐹 → ( ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) ↔ ( 𝐹 “ 𝐴 ) ⊆ ( 𝐵 ∩ ran 𝐹 ) ) )
3		inss1	⊢ ( 𝐵 ∩ ran 𝐹 ) ⊆ 𝐵
4		sstr2	⊢ ( ( 𝐹 “ 𝐴 ) ⊆ ( 𝐵 ∩ ran 𝐹 ) → ( ( 𝐵 ∩ ran 𝐹 ) ⊆ 𝐵 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ) )
5	3 4	mpi	⊢ ( ( 𝐹 “ 𝐴 ) ⊆ ( 𝐵 ∩ ran 𝐹 ) → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
6	2 5	biimtrdi	⊢ ( Fun 𝐹 → ( ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ) )
7		imass2	⊢ ( 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ ( ◡ 𝐹 “ 𝐵 ) ) )
8	6 7	impel	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )