suppofss1d

Description: Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019)

	Ref	Expression
Hypotheses	suppofssd.1	$⊢ φ \to A \in V$
	suppofssd.2	$⊢ φ \to Z \in B$
	suppofssd.3	$⊢ φ \to F : A ⟶ B$
	suppofssd.4	$⊢ φ \to G : A ⟶ B$
	suppofss1d.5	$⊢ (φ \land x \in B) \to Z X x = Z$
Assertion	suppofss1d	$⊢ φ \to (F X_{f} G) supp Z \subseteq F supp Z$

Proof

Step	Hyp	Ref	Expression
1		suppofssd.1	$⊢ φ \to A \in V$
2		suppofssd.2	$⊢ φ \to Z \in B$
3		suppofssd.3	$⊢ φ \to F : A ⟶ B$
4		suppofssd.4	$⊢ φ \to G : A ⟶ B$
5		suppofss1d.5	$⊢ (φ \land x \in B) \to Z X x = Z$
6	3	ffnd	$⊢ φ \to F Fn A$
7	4	ffnd	$⊢ φ \to G Fn A$
8		inidm	$⊢ A \cap A = A$
9		eqidd	$⊢ (φ \land y \in A) \to F (y) = F (y)$
10		eqidd	$⊢ (φ \land y \in A) \to G (y) = G (y)$
11	6 7 1 1 8 9 10	ofval	$⊢ (φ \land y \in A) \to (F X_{f} G) (y) = F (y) X G (y)$
12	11	adantr	$⊢ ((φ \land y \in A) \land F (y) = Z) \to (F X_{f} G) (y) = F (y) X G (y)$
13		simpr	$⊢ ((φ \land y \in A) \land F (y) = Z) \to F (y) = Z$
14	13	oveq1d	$⊢ ((φ \land y \in A) \land F (y) = Z) \to F (y) X G (y) = Z X G (y)$
15	5	ralrimiva	$⊢ φ \to \forall x \in B Z X x = Z$
16	15	adantr	$⊢ (φ \land y \in A) \to \forall x \in B Z X x = Z$
17	4	ffvelcdmda	$⊢ (φ \land y \in A) \to G (y) \in B$
18		simpr	$⊢ ((φ \land y \in A) \land x = G (y)) \to x = G (y)$
19	18	oveq2d	$⊢ ((φ \land y \in A) \land x = G (y)) \to Z X x = Z X G (y)$
20	19	eqeq1d	$⊢ ((φ \land y \in A) \land x = G (y)) \to (Z X x = Z \leftrightarrow Z X G (y) = Z)$
21	17 20	rspcdv	$⊢ (φ \land y \in A) \to (\forall x \in B Z X x = Z \to Z X G (y) = Z)$
22	16 21	mpd	$⊢ (φ \land y \in A) \to Z X G (y) = Z$
23	22	adantr	$⊢ ((φ \land y \in A) \land F (y) = Z) \to Z X G (y) = Z$
24	12 14 23	3eqtrd	$⊢ ((φ \land y \in A) \land F (y) = Z) \to (F X_{f} G) (y) = Z$
25	24	ex	$⊢ (φ \land y \in A) \to (F (y) = Z \to (F X_{f} G) (y) = Z)$
26	25	ralrimiva	$⊢ φ \to \forall y \in A (F (y) = Z \to (F X_{f} G) (y) = Z)$
27	6 7 1 1 8	offn	$⊢ φ \to (F X_{f} G) Fn A$
28		ssidd	$⊢ φ \to A \subseteq A$
29		suppfnss	$⊢ (((F X_{f} G) Fn A \land F Fn A) \land (A \subseteq A \land A \in V \land Z \in B)) \to (\forall y \in A (F (y) = Z \to (F X_{f} G) (y) = Z) \to (F X_{f} G) supp Z \subseteq F supp Z)$
30	27 6 28 1 2 29	syl23anc	$⊢ φ \to (\forall y \in A (F (y) = Z \to (F X_{f} G) (y) = Z) \to (F X_{f} G) supp Z \subseteq F supp Z)$
31	26 30	mpd	$⊢ φ \to (F X_{f} G) supp Z \subseteq F supp Z$

Metamath Proof Explorer

Theorem suppofss1d

Proof