Metamath Proof Explorer


Theorem ffs2

Description: Rewrite a function's support based with its range rather than the universal class. See also frnsuppeq . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypothesis ffs2.1 𝐶 = ( 𝐵 ∖ { 𝑍 } )
Assertion ffs2 ( ( 𝐴𝑉𝑍𝑊𝐹 : 𝐴𝐵 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹𝐶 ) )

Proof

Step Hyp Ref Expression
1 ffs2.1 𝐶 = ( 𝐵 ∖ { 𝑍 } )
2 frnsuppeq ( ( 𝐴𝑉𝑍𝑊 ) → ( 𝐹 : 𝐴𝐵 → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) ) )
3 2 3impia ( ( 𝐴𝑉𝑍𝑊𝐹 : 𝐴𝐵 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) )
4 1 imaeq2i ( 𝐹𝐶 ) = ( 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) )
5 3 4 eqtr4di ( ( 𝐴𝑉𝑍𝑊𝐹 : 𝐴𝐵 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹𝐶 ) )