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

Metamath Proof Explorer

Theorem imain

Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009)

Ref Expression
Assertion imain ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∩ ( 𝐹 “ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 imadif ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) )
2 imadif ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) )
3 2 difeq2d ⊢ ( Fun ◡ 𝐹 → ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ) )
4 1 3 eqtrd ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ) )
5 dfin4 ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )
6 5 imaeq2i ⊢ ( 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 “ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) )
7 dfin4 ⊢ ( ( 𝐹 “ 𝐴 ) ∩ ( 𝐹 “ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) )
8 4 6 7 3eqtr4g ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∩ ( 𝐹 “ 𝐵 ) ) )