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	birani	$⊢ (Fun G \land F \subseteq G) \to G Fn dom G$
6	3 5	jca	$⊢ (Fun G \land F \subseteq G) \to (F Fn dom F \land G Fn dom G)$
7	6	3adant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to (F Fn dom F \land G Fn dom G)$
8	7	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)$
9		dmss	$⊢ F \subseteq G \to dom F \subseteq dom G$
10	9	3ad2ant2	$⊢ (Fun G \land F \subseteq G \land G \in V) \to dom F \subseteq dom G$
11	10	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to dom F \subseteq dom G$
12		dmexg	$⊢ G \in V \to dom G \in V$
13	12	3ad2ant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to dom G \in V$
14	13	adantr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to dom G \in V$
15		simpr	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to Z \in V$
16	11 14 15	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)$
17	8 16	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))$
18		funssfv	$⊢ (Fun G \land F \subseteq G \land x \in dom F) \to G (x) = F (x)$
19	18	3expa	$⊢ ((Fun G \land F \subseteq G) \land x \in dom F) \to G (x) = F (x)$
20		eqeq1	$⊢ G (x) = F (x) \to (G (x) = Z \leftrightarrow F (x) = Z)$
21	20	biimpd	$⊢ G (x) = F (x) \to (G (x) = Z \to F (x) = Z)$
22	19 21	syl	$⊢ ((Fun G \land F \subseteq G) \land x \in dom F) \to (G (x) = Z \to F (x) = Z)$
23	22	ralrimiva	$⊢ (Fun G \land F \subseteq G) \to \forall x \in dom F (G (x) = Z \to F (x) = Z)$
24	23	3adant3	$⊢ (Fun G \land F \subseteq G \land G \in V) \to \forall x \in dom F (G (x) = Z \to F (x) = Z)$
25	24	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)$
26		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)$
27	17 25 26	sylc	$⊢ ((Fun G \land F \subseteq G \land G \in V) \land Z \in V) \to F supp Z \subseteq G supp Z$
28	27	expcom	$⊢ Z \in V \to ((Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z)$
29		ssid	$⊢ \emptyset \subseteq \emptyset$
30		simpr	$⊢ (F \in V \land Z \in V) \to Z \in V$
31		supp0prc	$⊢ \neg (F \in V \land Z \in V) \to F supp Z = \emptyset$
32	30 31	nsyl5	$⊢ \neg Z \in V \to F supp Z = \emptyset$
33		simpr	$⊢ (G \in V \land Z \in V) \to Z \in V$
34		supp0prc	$⊢ \neg (G \in V \land Z \in V) \to G supp Z = \emptyset$
35	33 34	nsyl5	$⊢ \neg Z \in V \to G supp Z = \emptyset$
36	32 35	sseq12d	$⊢ \neg Z \in V \to (F supp Z \subseteq G supp Z \leftrightarrow \emptyset \subseteq \emptyset)$
37	29 36	mpbiri	$⊢ \neg Z \in V \to F supp Z \subseteq G supp Z$
38	37	a1d	$⊢ \neg Z \in V \to ((Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z)$
39	28 38	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