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 \land F \in V \land Z \in W) \to F supp Z = F^{-1} [ran F ∖ \{Z\}]$

Step	Hyp	Ref	Expression
1		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
2	1	a1i	$⊢ (Fun F \land F \in V \land Z \in W) \to F^{-1} [ran F] = dom F$
3	2	difeq1d	$⊢ (Fun F \land F \in V \land Z \in W) \to F^{-1} [ran F] ∖ F^{-1} [\{Z\}] = dom F ∖ F^{-1} [\{Z\}]$
4		difpreima	$⊢ Fun F \to F^{-1} [ran F ∖ \{Z\}] = F^{-1} [ran F] ∖ F^{-1} [\{Z\}]$
5	4	3ad2ant1	$⊢ (Fun F \land F \in V \land Z \in W) \to F^{-1} [ran F ∖ \{Z\}] = F^{-1} [ran F] ∖ F^{-1} [\{Z\}]$
6		suppssdm	$⊢ F supp Z \subseteq dom F$
7		dfss4	$⊢ F supp Z \subseteq dom F \leftrightarrow 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 \land F \in V \land Z \in W) \to dom F ∖ {supp}_{Z} (F) = F^{-1} [\{Z\}]$
10	9	difeq2d	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F ∖ (dom F ∖ {supp}_{Z} (F)) = dom F ∖ F^{-1} [\{Z\}]$
11	8 10	eqtr3id	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = dom F ∖ F^{-1} [\{Z\}]$
12	3 5 11	3eqtr4rd	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = F^{-1} [ran F ∖ \{Z\}]$

Metamath Proof Explorer