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 𝐹 ∖ { 𝑍 } ) ) )