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		disjdif	$⊢ {supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)) = \emptyset$
9	8	a1i	$⊢ (Fun F \land F \in V \land Z \in W) \to {supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)) = \emptyset$
10		reldisjun	$⊢ (Rel F \land dom F = {supp}_{Z} (F) \cup (dom F ∖ {supp}_{Z} (F)) \land {supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)) = \emptyset) \to F = ({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
11	2 7 9 10	syl3anc	$⊢ (Fun F \land F \in V \land Z \in W) \to F = ({F ↾}_{{supp}_{Z} (F)}) \cup ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
12	11	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))})$
13		resss	$⊢ {F ↾}_{(dom F ∖ {supp}_{Z} (F))} \subseteq F$
14		sseqin2	$⊢ {F ↾}_{(dom F ∖ {supp}_{Z} (F))} \subseteq F \leftrightarrow F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{(dom F ∖ {supp}_{Z} (F))}$
15	13 14	mpbi	$⊢ F \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = {F ↾}_{(dom F ∖ {supp}_{Z} (F))}$
16		suppiniseg	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F ∖ {supp}_{Z} (F) = F^{-1} [\{Z\}]$
17	16	reseq2d	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{(dom F ∖ {supp}_{Z} (F))} = {F ↾}_{F^{-1} [\{Z\}]}$
18		cnvrescnv	$⊢ {({F^{-1} ↾}_{\{Z\}})}^{-1} = F \cap (V \times \{Z\})$
19		funcnvres2	$⊢ Fun F \to {({F^{-1} ↾}_{\{Z\}})}^{-1} = {F ↾}_{F^{-1} [\{Z\}]}$
20	18 19	eqtr3id	$⊢ Fun F \to F \cap (V \times \{Z\}) = {F ↾}_{F^{-1} [\{Z\}]}$
21	20	3ad2ant1	$⊢ (Fun F \land F \in V \land Z \in W) \to F \cap (V \times \{Z\}) = {F ↾}_{F^{-1} [\{Z\}]}$
22	17 21	eqtr4d	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{(dom F ∖ {supp}_{Z} (F))} = F \cap (V \times \{Z\})$
23	15 22	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\})$
24		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\})$
25	23 24	sylib	$⊢ (Fun F \land F \in V \land Z \in W) \to F ∖ ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = F ∖ (V \times \{Z\})$
26	8	reseq2i	$⊢ {F ↾}_{({supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)))} = {F ↾}_{\emptyset}$
27		resindi	$⊢ {F ↾}_{({supp}_{Z} (F) \cap (dom F ∖ {supp}_{Z} (F)))} = ({F ↾}_{{supp}_{Z} (F)}) \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))})$
28		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
29	26 27 28	3eqtr3i	$⊢ ({F ↾}_{{supp}_{Z} (F)}) \cap ({F ↾}_{(dom F ∖ {supp}_{Z} (F))}) = \emptyset$
30		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)}$
31	29 30	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)}$
32	12 25 31	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