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

Metamath Proof Explorer

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