fressupp

Description: The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

		Ref	Expression
	Assertion	fressupp	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{{supp}_{Z} (F)} = F ∖ (V \times \{Z\})$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2	1	3ad2ant1	$⊢ (Fun F \land F \in V \land Z \in W) \to Rel F$
3		suppssdm	$⊢ F supp Z \subseteq dom F$
4		undif	$⊢ F supp Z \subseteq dom F \leftrightarrow {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F)) = dom F$
5	4	biimpi	$⊢ F supp Z \subseteq dom F \to {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F)) = dom F$
6	5	eqcomd	$⊢ F supp Z \subseteq dom F \to dom F = {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F))$
7	3 6	mp1i	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F = {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F))$
8		reldmun	$⊢ (Rel F \land dom F = {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F))) \to F = ({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
9	2 7 8	syl2anc	$⊢ (Fun F \land F \in V \land Z \in W) \to F = ({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
10	9	difeq1d	$⊢ (Fun F \land F \in V \land Z \in W) \to F ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = (({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})) ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
11		resss	$⊢ {F ↾}_{(dom F ∖ {supp}_{Z} (F))} \subseteq F$
12		sseqin2	$⊢ {F ↾}_{(dom F ∖ {supp}_{Z} (F))} \subseteq F \leftrightarrow F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{(dom F ∖ {supp}_{Z} (F))}$
13	11 12	mpbi	$⊢ F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{(dom F ∖ {supp}_{Z} (F))}$
14		suppiniseg	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F ∖ {supp}_{Z} (F) = F^{-1} [\{Z\}]$
15	14	reseq2d	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{(dom F ∖ {supp}_{Z} (F))} = {F ↾}_{F^{-1} [\{Z\}]}$
16		cnvrescnv	$⊢ {({F^{-1} ↾}_{\{Z\}})}^{-1} = F \cap (V \times \{Z\})$
17		funcnvres2	$⊢ Fun F \to {({F^{-1} ↾}_{\{Z\}})}^{-1} = {F ↾}_{F^{-1} [\{Z\}]}$
18	16 17	eqtr3id	$⊢ Fun F \to F \cap (V \times \{Z\}) = {F ↾}_{F^{-1} [\{Z\}]}$
19	18	3ad2ant1	$⊢ (Fun F \land F \in V \land Z \in W) \to F \cap (V \times \{Z\}) = {F ↾}_{F^{-1} [\{Z\}]}$
20	15 19	eqtr4d	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{(dom F ∖ {supp}_{Z} (F))} = F \cap (V \times \{Z\})$
21	13 20	eqtrid	$⊢ (Fun F \land F \in V \land Z \in W) \to F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = F \cap (V \times \{Z\})$
22		indifbi	$⊢ F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = F \cap (V \times \{Z\}) \leftrightarrow F ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = F ∖ (V \times \{Z\})$
23	21 22	sylib	$⊢ (Fun F \land F \in V \land Z \in W) \to F ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = F ∖ (V \times \{Z\})$
24		disjdif	$⊢ {supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)) = \emptyset$
25	24	reseq2i	$⊢ {F ↾}_{({supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)))} = {F ↾}_{\emptyset}$
26		resindi	$⊢ {F ↾}_{({supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)))} = ({F ↾}_{{supp}_{Z} (F)}) \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
27		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
28	25 26 27	3eqtr3i	$⊢ ({F ↾}_{{supp}_{Z} (F)}) \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = \emptyset$
29		undif5	$⊢ ({F ↾}_{{supp}_{Z} (F)}) \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = \emptyset \to (({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})) ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{{supp}_{Z} (F)}$
30	28 29	mp1i	$⊢ (Fun F \land F \in V \land Z \in W) \to (({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})) ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{{supp}_{Z} (F)}$
31	10 23 30	3eqtr3rd	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{{supp}_{Z} (F)} = F ∖ (V \times \{Z\})$

Metamath Proof Explorer

Theorem fressupp

Proof