ressuppssdif

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	ressuppssdif	$⊢ (F \in V \land Z \in W) \to F supp Z \subseteq {supp}_{Z} (({F ↾}_{B})) \cup (dom F ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (\{z \in dom F \| F [\{z\}] \neq \{Z\}\} ∖ \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}) \leftrightarrow (x \in \{z \in dom F \| F [\{z\}] \neq \{Z\}\} \land \neg x \in \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\})$
2		sneq	$⊢ z = x \to \{z\} = \{x\}$
3	2	imaeq2d	$⊢ z = x \to F [\{z\}] = F [\{x\}]$
4	3	neeq1d	$⊢ z = x \to (F [\{z\}] \neq \{Z\} \leftrightarrow F [\{x\}] \neq \{Z\})$
5	4	elrab	$⊢ x \in \{z \in dom F \| F [\{z\}] \neq \{Z\}\} \leftrightarrow (x \in dom F \land F [\{x\}] \neq \{Z\})$
6		ianor	$⊢ \neg (x \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{x\}] \neq \{Z\}) \leftrightarrow (\neg x \in dom ({F ↾}_{B}) \lor \neg ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
7	2	imaeq2d	$⊢ z = x \to ({F ↾}_{B}) [\{z\}] = ({F ↾}_{B}) [\{x\}]$
8	7	neeq1d	$⊢ z = x \to (({F ↾}_{B}) [\{z\}] \neq \{Z\} \leftrightarrow ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
9	8	elrab	$⊢ x \in \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \leftrightarrow (x \in dom ({F ↾}_{B}) \land ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
10	6 9	xchnxbir	$⊢ \neg x \in \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \leftrightarrow (\neg x \in dom ({F ↾}_{B}) \lor \neg ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
11		ianor	$⊢ \neg (x \in B \land x \in dom F) \leftrightarrow (\neg x \in B \lor \neg x \in dom F)$
12		dmres	$⊢ dom ({F ↾}_{B}) = B \cap dom F$
13	12	elin2	$⊢ x \in dom ({F ↾}_{B}) \leftrightarrow (x \in B \land x \in dom F)$
14	11 13	xchnxbir	$⊢ \neg x \in dom ({F ↾}_{B}) \leftrightarrow (\neg x \in B \lor \neg x \in dom F)$
15		simpl	$⊢ (x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in dom F$
16	15	anim2i	$⊢ (\neg x \in B \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to (\neg x \in B \land x \in dom F)$
17	16	ancomd	$⊢ (\neg x \in B \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to (x \in dom F \land \neg x \in B)$
18		eldif	$⊢ x \in (dom F ∖ B) \leftrightarrow (x \in dom F \land \neg x \in B)$
19	17 18	sylibr	$⊢ (\neg x \in B \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to x \in (dom F ∖ B)$
20	19	ex	$⊢ \neg x \in B \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
21		pm2.24	$⊢ x \in dom F \to (\neg x \in dom F \to x \in (dom F ∖ B))$
22	21	adantr	$⊢ (x \in dom F \land F [\{x\}] \neq \{Z\}) \to (\neg x \in dom F \to x \in (dom F ∖ B))$
23	22	com12	$⊢ \neg x \in dom F \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
24	20 23	jaoi	$⊢ (\neg x \in B \lor \neg x \in dom F) \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
25	14 24	sylbi	$⊢ \neg x \in dom ({F ↾}_{B}) \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
26	15	adantl	$⊢ (\neg ({F ↾}_{B}) [\{x\}] \neq \{Z\} \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to x \in dom F$
27		snssi	$⊢ x \in B \to \{x\} \subseteq B$
28	27	adantl	$⊢ (x \in dom F \land x \in B) \to \{x\} \subseteq B$
29		resima2	$⊢ \{x\} \subseteq B \to ({F ↾}_{B}) [\{x\}] = F [\{x\}]$
30	28 29	syl	$⊢ (x \in dom F \land x \in B) \to ({F ↾}_{B}) [\{x\}] = F [\{x\}]$
31	30	eqcomd	$⊢ (x \in dom F \land x \in B) \to F [\{x\}] = ({F ↾}_{B}) [\{x\}]$
32	31	adantr	$⊢ ((x \in dom F \land x \in B) \land ({F ↾}_{B}) [\{x\}] = \{Z\}) \to F [\{x\}] = ({F ↾}_{B}) [\{x\}]$
33		simpr	$⊢ ((x \in dom F \land x \in B) \land ({F ↾}_{B}) [\{x\}] = \{Z\}) \to ({F ↾}_{B}) [\{x\}] = \{Z\}$
34	32 33	eqtrd	$⊢ ((x \in dom F \land x \in B) \land ({F ↾}_{B}) [\{x\}] = \{Z\}) \to F [\{x\}] = \{Z\}$
35	34	ex	$⊢ (x \in dom F \land x \in B) \to (({F ↾}_{B}) [\{x\}] = \{Z\} \to F [\{x\}] = \{Z\})$
36	35	necon3d	$⊢ (x \in dom F \land x \in B) \to (F [\{x\}] \neq \{Z\} \to ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
37	36	impancom	$⊢ (x \in dom F \land F [\{x\}] \neq \{Z\}) \to (x \in B \to ({F ↾}_{B}) [\{x\}] \neq \{Z\})$
38	37	con3d	$⊢ (x \in dom F \land F [\{x\}] \neq \{Z\}) \to (\neg ({F ↾}_{B}) [\{x\}] \neq \{Z\} \to \neg x \in B)$
39	38	impcom	$⊢ (\neg ({F ↾}_{B}) [\{x\}] \neq \{Z\} \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to \neg x \in B$
40	26 39	eldifd	$⊢ (\neg ({F ↾}_{B}) [\{x\}] \neq \{Z\} \land (x \in dom F \land F [\{x\}] \neq \{Z\})) \to x \in (dom F ∖ B)$
41	40	ex	$⊢ \neg ({F ↾}_{B}) [\{x\}] \neq \{Z\} \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
42	25 41	jaoi	$⊢ (\neg x \in dom ({F ↾}_{B}) \lor \neg ({F ↾}_{B}) [\{x\}] \neq \{Z\}) \to ((x \in dom F \land F [\{x\}] \neq \{Z\}) \to x \in (dom F ∖ B))$
43	42	impcom	$⊢ ((x \in dom F \land F [\{x\}] \neq \{Z\}) \land (\neg x \in dom ({F ↾}_{B}) \lor \neg ({F ↾}_{B}) [\{x\}] \neq \{Z\})) \to x \in (dom F ∖ B)$
44	5 10 43	syl2anb	$⊢ (x \in \{z \in dom F \| F [\{z\}] \neq \{Z\}\} \land \neg x \in \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}) \to x \in (dom F ∖ B)$
45	1 44	sylbi	$⊢ x \in (\{z \in dom F \| F [\{z\}] \neq \{Z\}\} ∖ \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}) \to x \in (dom F ∖ B)$
46	45	a1i	$⊢ (F \in V \land Z \in W) \to (x \in (\{z \in dom F \| F [\{z\}] \neq \{Z\}\} ∖ \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}) \to x \in (dom F ∖ B))$
47	46	ssrdv	$⊢ (F \in V \land Z \in W) \to \{z \in dom F \| F [\{z\}] \neq \{Z\}\} ∖ \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \subseteq dom F ∖ B$
48		ssundif	$⊢ \{z \in dom F \| F [\{z\}] \neq \{Z\}\} \subseteq \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \cup (dom F ∖ B) \leftrightarrow \{z \in dom F \| F [\{z\}] \neq \{Z\}\} ∖ \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \subseteq dom F ∖ B$
49	47 48	sylibr	$⊢ (F \in V \land Z \in W) \to \{z \in dom F \| F [\{z\}] \neq \{Z\}\} \subseteq \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \cup (dom F ∖ B)$
50		suppval	$⊢ (F \in V \land Z \in W) \to F supp Z = \{z \in dom F \| F [\{z\}] \neq \{Z\}\}$
51		resexg	$⊢ F \in V \to {F ↾}_{B} \in V$
52		suppval	$⊢ ({F ↾}_{B} \in V \land Z \in W) \to ({F ↾}_{B}) supp Z = \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}$
53	51 52	sylan	$⊢ (F \in V \land Z \in W) \to ({F ↾}_{B}) supp Z = \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\}$
54	53	uneq1d	$⊢ (F \in V \land Z \in W) \to {supp}_{Z} (({F ↾}_{B})) \cup (dom F ∖ B) = \{z \in dom ({F ↾}_{B}) \| ({F ↾}_{B}) [\{z\}] \neq \{Z\}\} \cup (dom F ∖ B)$
55	49 50 54	3sstr4d	$⊢ (F \in V \land Z \in W) \to F supp Z \subseteq {supp}_{Z} (({F ↾}_{B})) \cup (dom F ∖ B)$

Metamath Proof Explorer

Theorem ressuppssdif

Proof