suppofss2d

Description: Condition for the support of a function operation to be a subset of the support of the right 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$
	suppofss2d.5	$⊢ (φ \land x \in B) \to x X Z = Z$
Assertion	suppofss2d	$⊢ φ \to (F X_{f} G) supp Z \subseteq G 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		suppofss2d.5	$⊢ (φ \land x \in B) \to x X Z = 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 G (y) = Z) \to (F X_{f} G) (y) = F (y) X G (y)$
13		simpr	$⊢ ((φ \land y \in A) \land G (y) = Z) \to G (y) = Z$
14	13	oveq2d	$⊢ ((φ \land y \in A) \land G (y) = Z) \to F (y) X G (y) = F (y) X Z$
15	5	ralrimiva	$⊢ φ \to \forall x \in B x X Z = Z$
16	15	adantr	$⊢ (φ \land y \in A) \to \forall x \in B x X Z = Z$
17	3	ffvelcdmda	$⊢ (φ \land y \in A) \to F (y) \in B$
18		simpr	$⊢ ((φ \land y \in A) \land x = F (y)) \to x = F (y)$
19	18	oveq1d	$⊢ ((φ \land y \in A) \land x = F (y)) \to x X Z = F (y) X Z$
20	19	eqeq1d	$⊢ ((φ \land y \in A) \land x = F (y)) \to (x X Z = Z \leftrightarrow F (y) X Z = Z)$
21	17 20	rspcdv	$⊢ (φ \land y \in A) \to (\forall x \in B x X Z = Z \to F (y) X Z = Z)$
22	16 21	mpd	$⊢ (φ \land y \in A) \to F (y) X Z = Z$
23	22	adantr	$⊢ ((φ \land y \in A) \land G (y) = Z) \to F (y) X Z = Z$
24	12 14 23	3eqtrd	$⊢ ((φ \land y \in A) \land G (y) = Z) \to (F X_{f} G) (y) = Z$
25	24	ex	$⊢ (φ \land y \in A) \to (G (y) = Z \to (F X_{f} G) (y) = Z)$
26	25	ralrimiva	$⊢ φ \to \forall y \in A (G (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 G Fn A) \land (A \subseteq A \land A \in V \land Z \in B)) \to (\forall y \in A (G (y) = Z \to (F X_{f} G) (y) = Z) \to (F X_{f} G) supp Z \subseteq G supp Z)$
30	27 7 28 1 2 29	syl23anc	$⊢ φ \to (\forall y \in A (G (y) = Z \to (F X_{f} G) (y) = Z) \to (F X_{f} G) supp Z \subseteq G supp Z)$
31	26 30	mpd	$⊢ φ \to (F X_{f} G) supp Z \subseteq G supp Z$

Metamath Proof Explorer

Theorem suppofss2d

Proof