Metamath Proof Explorer


Theorem supppreima

Description: Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024)

Ref Expression
Assertion supppreima ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 cnvimarndm ( 𝐹 “ ran 𝐹 ) = dom 𝐹
2 1 a1i ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( 𝐹 “ ran 𝐹 ) = dom 𝐹 )
3 2 difeq1d ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( ( 𝐹 “ ran 𝐹 ) ∖ ( 𝐹 “ { 𝑍 } ) ) = ( dom 𝐹 ∖ ( 𝐹 “ { 𝑍 } ) ) )
4 difpreima ( Fun 𝐹 → ( 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) = ( ( 𝐹 “ ran 𝐹 ) ∖ ( 𝐹 “ { 𝑍 } ) ) )
5 4 3ad2ant1 ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) = ( ( 𝐹 “ ran 𝐹 ) ∖ ( 𝐹 “ { 𝑍 } ) ) )
6 suppssdm ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹
7 dfss4 ( ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 ) )
8 6 7 mpbi ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 )
9 suppiniseg ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( 𝐹 “ { 𝑍 } ) )
10 9 difeq2d ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( dom 𝐹 ∖ ( 𝐹 “ { 𝑍 } ) ) )
11 8 10 eqtr3id ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( 𝐹 supp 𝑍 ) = ( dom 𝐹 ∖ ( 𝐹 “ { 𝑍 } ) ) )
12 3 5 11 3eqtr4rd ( ( Fun 𝐹𝐹𝑉𝑍𝑊 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) )