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 ⁡ F ∧ F ∈ V ∧ Z ∈ W → F supp Z = F -1 ran ⁡ F ∖ Z

Proof

Step Hyp Ref Expression
1 cnvimarndm ⊢ F -1 ran ⁡ F = dom ⁡ F
2 1 a1i ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F -1 ran ⁡ F = dom ⁡ F
3 2 difeq1d ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F -1 ran ⁡ F ∖ F -1 Z = dom ⁡ F ∖ F -1 Z
4 difpreima ⊢ Fun ⁡ F → F -1 ran ⁡ F ∖ Z = F -1 ran ⁡ F ∖ F -1 Z
5 4 3ad2ant1 ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F -1 ran ⁡ F ∖ Z = F -1 ran ⁡ F ∖ F -1 Z
6 suppssdm ⊢ F supp Z ⊆ dom ⁡ F
7 dfss4 ⊢ F supp Z ⊆ dom ⁡ F ↔ dom ⁡ F ∖ dom ⁡ F ∖ supp Z⁡ F = F supp Z
8 6 7 mpbi ⊢ dom ⁡ F ∖ dom ⁡ F ∖ supp Z⁡ F = F supp Z
9 suppiniseg ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → dom ⁡ F ∖ supp Z⁡ F = F -1 Z
10 9 difeq2d ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → dom ⁡ F ∖ dom ⁡ F ∖ supp Z⁡ F = dom ⁡ F ∖ F -1 Z
11 8 10 eqtr3id ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F supp Z = dom ⁡ F ∖ F -1 Z
12 3 5 11 3eqtr4rd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F supp Z = F -1 ran ⁡ F ∖ Z