funsssuppss

Description: The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019)

		Ref	Expression
	Assertion	funsssuppss	$⊢ (Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z$

Proof

Step	Hyp	Ref	Expression
1		funss	$⊢ F \subseteq G \to (Fun G \to Fun F)$
2	1	impcom	$⊢ (Fun G \land F \subseteq G) \to Fun F$
3	2	funfnd	$⊢ (Fun G \land F \subseteq G) \to F Fn dom F$
4		funfn	$⊢ Fun G \leftrightarrow G Fn dom G$
5	4	biimpi	$⊢ Fun G \to G Fn dom G$
6	5	adantr	$⊢ (Fun G \land F \subseteq G) \to G Fn dom G$
7	3 6	jca	$⊢ (Fun G \land F \subseteq G) \to (F Fn dom F \land G Fn dom G)$
8	7	3adant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to (F Fn dom F \land G Fn dom G)$
9	8	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to (F Fn dom F \land G Fn dom G)$
10		dmss	$⊢ F \subseteq G \to dom F \subseteq dom G$
11	10	3ad2ant2	$⊢ (Fun G \land F \subseteq G \land G \in V) \to dom F \subseteq dom G$
12	11	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to dom F \subseteq dom G$
13		dmexg	$⊢ G \in V \to dom G \in V$
14	13	3ad2ant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to dom G \in V$
15	14	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to dom G \in V$
16		simpr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to Z \in V$
17	12 15 16	3jca	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to (dom F \subseteq dom G \land dom G \in V \land Z \in V)$
18	9 17	jca	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to ((F Fn dom F \land G Fn dom G) \land (dom F \subseteq dom G \land dom G \in V \land Z \in V))$
19		funssfv	$⊢ (Fun G \land F \subseteq G \land x \in dom F) \to G (x) = F (x)$
20	19	3expa	$⊢ ((Fun G \land F \subseteq G) \land x \in dom F) \to G (x) = F (x)$
21		eqeq1	$⊢ G (x) = F (x) \to (G (x) = Z \leftrightarrow F (x) = Z)$
22	21	biimpd	$⊢ G (x) = F (x) \to (G (x) = Z \to F (x) = Z)$
23	20 22	syl	$⊢ ((Fun G \land F \subseteq G) \land x \in dom F) \to (G (x) = Z \to F (x) = Z)$
24	23	ralrimiva	$⊢ (Fun G \land F \subseteq G) \to \forall x \in dom F (G (x) = Z \to F (x) = Z)$
25	24	3adant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to \forall x \in dom F (G (x) = Z \to F (x) = Z)$
26	25	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to \forall x \in dom F (G (x) = Z \to F (x) = Z)$
27		suppfnss	$⊢ ((F Fn dom F \land G Fn dom G) \land (dom F \subseteq dom G \land dom G \in V \land Z \in V)) \to (\forall x \in dom F (G (x) = Z \to F (x) = Z) \to F supp Z \subseteq G supp Z)$
28	18 26 27	sylc	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to F supp Z \subseteq G supp Z$
29	28	expcom	$⊢ Z \in V \to ((Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z)$
30		ssid	$⊢ \emptyset \subseteq \emptyset$
31		simpr	$⊢ (F \in V \land Z \in V) \to Z \in V$
32		supp0prc	$⊢ \neg (F \in V \land Z \in V) \to F supp Z = \emptyset$
33	31 32	nsyl5	$⊢ \neg Z \in V \to F supp Z = \emptyset$
34		simpr	$⊢ (G \in V \land Z \in V) \to Z \in V$
35		supp0prc	$⊢ \neg (G \in V \land Z \in V) \to G supp Z = \emptyset$
36	34 35	nsyl5	$⊢ \neg Z \in V \to G supp Z = \emptyset$
37	33 36	sseq12d	$⊢ \neg Z \in V \to (F supp Z \subseteq G supp Z \leftrightarrow \emptyset \subseteq \emptyset)$
38	30 37	mpbiri	$⊢ \neg Z \in V \to F supp Z \subseteq G supp Z$
39	38	a1d	$⊢ \neg Z \in V \to ((Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z)$
40	29 39	pm2.61i	$⊢ (Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z$

Metamath Proof Explorer

Theorem funsssuppss

Proof