suppfnss

Description: The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 6-Jun-2022)

		Ref	Expression
	Assertion	suppfnss	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (\forall x \in A (G (x) = Z \to F (x) = Z) \to F supp Z \subseteq G supp Z)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to A \subseteq B$
2		fndm	$⊢ F Fn A \to dom F = A$
3	2	ad2antrr	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to dom F = A$
4		fndm	$⊢ G Fn B \to dom G = B$
5	4	ad2antlr	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to dom G = B$
6	1 3 5	3sstr4d	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to dom F \subseteq dom G$
7	6	adantr	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to dom F \subseteq dom G$
8	2	eleq2d	$⊢ F Fn A \to (y \in dom F \leftrightarrow y \in A)$
9	8	ad2antrr	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (y \in dom F \leftrightarrow y \in A)$
10		fveqeq2	$⊢ x = y \to (G (x) = Z \leftrightarrow G (y) = Z)$
11		fveqeq2	$⊢ x = y \to (F (x) = Z \leftrightarrow F (y) = Z)$
12	10 11	imbi12d	$⊢ x = y \to ((G (x) = Z \to F (x) = Z) \leftrightarrow (G (y) = Z \to F (y) = Z))$
13	12	rspcv	$⊢ y \in A \to (\forall x \in A (G (x) = Z \to F (x) = Z) \to (G (y) = Z \to F (y) = Z))$
14	9 13	syl6bi	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (y \in dom F \to (\forall x \in A (G (x) = Z \to F (x) = Z) \to (G (y) = Z \to F (y) = Z)))$
15	14	com23	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (\forall x \in A (G (x) = Z \to F (x) = Z) \to (y \in dom F \to (G (y) = Z \to F (y) = Z)))$
16	15	imp31	$⊢ ((((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \land y \in dom F) \to (G (y) = Z \to F (y) = Z)$
17	16	necon3d	$⊢ ((((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \land y \in dom F) \to (F (y) \neq Z \to G (y) \neq Z)$
18	17	ex	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to (y \in dom F \to (F (y) \neq Z \to G (y) \neq Z))$
19	18	com23	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to (F (y) \neq Z \to (y \in dom F \to G (y) \neq Z))$
20	19	3imp	$⊢ ((((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \land F (y) \neq Z \land y \in dom F) \to G (y) \neq Z$
21	7 20	rabssrabd	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to \{y \in dom F \| F (y) \neq Z\} \subseteq \{y \in dom G \| G (y) \neq Z\}$
22		fnfun	$⊢ F Fn A \to Fun F$
23	22	ad2antrr	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to Fun F$
24		simpl	$⊢ (F Fn A \land G Fn B) \to F Fn A$
25		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
26	25	3adant3	$⊢ (A \subseteq B \land B \in V \land Z \in W) \to A \in V$
27		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
28	24 26 27	syl2an	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to F \in V$
29		simpr3	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to Z \in W$
30		suppval1	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = \{y \in dom F \| F (y) \neq Z\}$
31	23 28 29 30	syl3anc	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to F supp Z = \{y \in dom F \| F (y) \neq Z\}$
32		fnfun	$⊢ G Fn B \to Fun G$
33	32	ad2antlr	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to Fun G$
34		simpr	$⊢ (F Fn A \land G Fn B) \to G Fn B$
35		simp2	$⊢ (A \subseteq B \land B \in V \land Z \in W) \to B \in V$
36		fnex	$⊢ (G Fn B \land B \in V) \to G \in V$
37	34 35 36	syl2an	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to G \in V$
38		suppval1	$⊢ (Fun G \land G \in V \land Z \in W) \to G supp Z = \{y \in dom G \| G (y) \neq Z\}$
39	33 37 29 38	syl3anc	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to G supp Z = \{y \in dom G \| G (y) \neq Z\}$
40	31 39	sseq12d	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (F supp Z \subseteq G supp Z \leftrightarrow \{y \in dom F \| F (y) \neq Z\} \subseteq \{y \in dom G \| G (y) \neq Z\})$
41	40	adantr	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to (F supp Z \subseteq G supp Z \leftrightarrow \{y \in dom F \| F (y) \neq Z\} \subseteq \{y \in dom G \| G (y) \neq Z\})$
42	21 41	mpbird	$⊢ (((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \land \forall x \in A (G (x) = Z \to F (x) = Z)) \to F supp Z \subseteq G supp Z$
43	42	ex	$⊢ ((F Fn A \land G Fn B) \land (A \subseteq B \land B \in V \land Z \in W)) \to (\forall x \in A (G (x) = Z \to F (x) = Z) \to F supp Z \subseteq G supp Z)$

Metamath Proof Explorer

Theorem suppfnss

Proof