ressuppss

Description: The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019)

		Ref	Expression
	Assertion	ressuppss	$⊢ (F \in V \land Z \in W) \to ({F ↾}_{B}) supp Z \subseteq F supp Z$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$⊢ b \in (B \cap dom F) \to b \in dom F$
2		dmres	$⊢ dom ({F ↾}_{B}) = B \cap dom F$
3	1 2	eleq2s	$⊢ b \in dom ({F ↾}_{B}) \to b \in dom F$
4	3	ad2antrl	$⊢ ((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to b \in dom F$
5		snssi	$⊢ b \in B \to \{b\} \subseteq B$
6		resima2	$⊢ \{b\} \subseteq B \to ({F ↾}_{B}) [\{b\}] = F [\{b\}]$
7	5 6	syl	$⊢ b \in B \to ({F ↾}_{B}) [\{b\}] = F [\{b\}]$
8	7	neeq1d	$⊢ b \in B \to (({F ↾}_{B}) [\{b\}] \neq \{Z\} \leftrightarrow F [\{b\}] \neq \{Z\})$
9	8	biimpd	$⊢ b \in B \to (({F ↾}_{B}) [\{b\}] \neq \{Z\} \to F [\{b\}] \neq \{Z\})$
10	9	adantld	$⊢ b \in B \to ((b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\}) \to F [\{b\}] \neq \{Z\})$
11	10	adantld	$⊢ b \in B \to (((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to F [\{b\}] \neq \{Z\})$
12		elin	$⊢ b \in (B \cap dom F) \leftrightarrow (b \in B \land b \in dom F)$
13		pm2.24	$⊢ b \in B \to (\neg b \in B \to F [\{b\}] \neq \{Z\})$
14	13	adantr	$⊢ (b \in B \land b \in dom F) \to (\neg b \in B \to F [\{b\}] \neq \{Z\})$
15	12 14	sylbi	$⊢ b \in (B \cap dom F) \to (\neg b \in B \to F [\{b\}] \neq \{Z\})$
16	15 2	eleq2s	$⊢ b \in dom ({F ↾}_{B}) \to (\neg b \in B \to F [\{b\}] \neq \{Z\})$
17	16	ad2antrl	$⊢ ((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to (\neg b \in B \to F [\{b\}] \neq \{Z\})$
18	17	com12	$⊢ \neg b \in B \to (((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to F [\{b\}] \neq \{Z\})$
19	11 18	pm2.61i	$⊢ ((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to F [\{b\}] \neq \{Z\}$
20	4 19	jca	$⊢ ((F \in V \land Z \in W) \land (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})) \to (b \in dom F \land F [\{b\}] \neq \{Z\})$
21	20	ex	$⊢ (F \in V \land Z \in W) \to ((b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\}) \to (b \in dom F \land F [\{b\}] \neq \{Z\}))$
22	21	ss2abdv	$⊢ (F \in V \land Z \in W) \to \{b \| (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})\} \subseteq \{b \| (b \in dom F \land F [\{b\}] \neq \{Z\})\}$
23		df-rab	$⊢ \{b \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{b\}] \neq \{Z\}\} = \{b \| (b \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{b\}] \neq \{Z\})\}$
24		df-rab	$⊢ \{b \in dom F \| F [\{b\}] \neq \{Z\}\} = \{b \| (b \in dom F \land F [\{b\}] \neq \{Z\})\}$
25	22 23 24	3sstr4g	$⊢ (F \in V \land Z \in W) \to \{b \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{b\}] \neq \{Z\}\} \subseteq \{b \in dom F \| F [\{b\}] \neq \{Z\}\}$
26		resexg	$⊢ F \in V \to {F ↾}_{B} \in V$
27		suppval	$⊢ ({F ↾}_{B} \in V \land Z \in W) \to ({F ↾}_{B}) supp Z = \{b \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{b\}] \neq \{Z\}\}$
28	26 27	sylan	$⊢ (F \in V \land Z \in W) \to ({F ↾}_{B}) supp Z = \{b \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{b\}] \neq \{Z\}\}$
29		suppval	$⊢ (F \in V \land Z \in W) \to F supp Z = \{b \in dom F \| F [\{b\}] \neq \{Z\}\}$
30	25 28 29	3sstr4d	$⊢ (F \in V \land Z \in W) \to ({F ↾}_{B}) supp Z \subseteq F supp Z$

Metamath Proof Explorer

Theorem ressuppss

Proof