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

Metamath Proof Explorer

Theorem cnvimainrn

Description: The preimage of the intersection of the range of a class and a class A is the preimage of the class A . (Contributed by AV, 17-Sep-2024)

Ref Expression
Assertion cnvimainrn ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∩ ( ◡ 𝐹 “ 𝐴 ) ) )
2 cnvimass ⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
3 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
4 2 3 sseqtrri ⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 )
5 dfss2 ⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 ) ↔ ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝐴 ) )
6 4 5 mpbi ⊢ ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝐴 )
7 6 ineqcomi ⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∩ ( ◡ 𝐹 “ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 )
8 1 7 eqtrdi ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 ) )