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

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