This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) → ( ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 → 𝐴 ⊆ ( 𝐹 “ 𝐵 ) ) )