suppofssd

Description: Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023)

	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$
	suppofssd.5	$⊢ φ \to Z X Z = Z$
Assertion	suppofssd	$⊢ φ \to (F X_{f} G) supp Z \subseteq {supp}_{Z} (F) \cup {supp}_{Z} (G)$

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		suppofssd.5	$⊢ φ \to Z X Z = Z$
6		ovexd	$⊢ (φ \land (x \in B \land y \in B)) \to x X y \in V$
7		inidm	$⊢ A \cap A = A$
8	6 3 4 1 1 7	off	$⊢ φ \to (F X_{f} G) : A ⟶ V$
9		eldif	$⊢ k \in (A ∖ ({supp}_{Z} (F) \cup {supp}_{Z} (G))) \leftrightarrow (k \in A \land \neg k \in ({supp}_{Z} (F) \cup {supp}_{Z} (G)))$
10		ioran	$⊢ \neg (k \in {supp}_{Z} (F) \lor k \in {supp}_{Z} (G)) \leftrightarrow (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G))$
11		elun	$⊢ k \in ({supp}_{Z} (F) \cup {supp}_{Z} (G)) \leftrightarrow (k \in {supp}_{Z} (F) \lor k \in {supp}_{Z} (G))$
12	10 11	xchnxbir	$⊢ \neg k \in ({supp}_{Z} (F) \cup {supp}_{Z} (G)) \leftrightarrow (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G))$
13	12	anbi2i	$⊢ (k \in A \land \neg k \in ({supp}_{Z} (F) \cup {supp}_{Z} (G))) \leftrightarrow (k \in A \land (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G)))$
14	9 13	bitri	$⊢ k \in (A ∖ ({supp}_{Z} (F) \cup {supp}_{Z} (G))) \leftrightarrow (k \in A \land (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G)))$
15	3	ffnd	$⊢ φ \to F Fn A$
16		elsuppfn	$⊢ (F Fn A \land A \in V \land Z \in B) \to (k \in {supp}_{Z} (F) \leftrightarrow (k \in A \land F (k) \neq Z))$
17	15 1 2 16	syl3anc	$⊢ φ \to (k \in {supp}_{Z} (F) \leftrightarrow (k \in A \land F (k) \neq Z))$
18	17	notbid	$⊢ φ \to (\neg k \in {supp}_{Z} (F) \leftrightarrow \neg (k \in A \land F (k) \neq Z))$
19	18	biimpd	$⊢ φ \to (\neg k \in {supp}_{Z} (F) \to \neg (k \in A \land F (k) \neq Z))$
20	4	ffnd	$⊢ φ \to G Fn A$
21		elsuppfn	$⊢ (G Fn A \land A \in V \land Z \in B) \to (k \in {supp}_{Z} (G) \leftrightarrow (k \in A \land G (k) \neq Z))$
22	20 1 2 21	syl3anc	$⊢ φ \to (k \in {supp}_{Z} (G) \leftrightarrow (k \in A \land G (k) \neq Z))$
23	22	notbid	$⊢ φ \to (\neg k \in {supp}_{Z} (G) \leftrightarrow \neg (k \in A \land G (k) \neq Z))$
24	23	biimpd	$⊢ φ \to (\neg k \in {supp}_{Z} (G) \to \neg (k \in A \land G (k) \neq Z))$
25	19 24	anim12d	$⊢ φ \to ((\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G)) \to (\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z)))$
26	25	anim2d	$⊢ φ \to ((k \in A \land (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G))) \to (k \in A \land (\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z))))$
27	26	imp	$⊢ (φ \land (k \in A \land (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G)))) \to (k \in A \land (\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z)))$
28		pm3.2	$⊢ k \in A \to (F (k) \neq Z \to (k \in A \land F (k) \neq Z))$
29	28	necon1bd	$⊢ k \in A \to (\neg (k \in A \land F (k) \neq Z) \to F (k) = Z)$
30		pm3.2	$⊢ k \in A \to (G (k) \neq Z \to (k \in A \land G (k) \neq Z))$
31	30	necon1bd	$⊢ k \in A \to (\neg (k \in A \land G (k) \neq Z) \to G (k) = Z)$
32	29 31	anim12d	$⊢ k \in A \to ((\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z)) \to (F (k) = Z \land G (k) = Z))$
33	32	imdistani	$⊢ (k \in A \land (\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z))) \to (k \in A \land (F (k) = Z \land G (k) = Z))$
34	15	adantr	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to F Fn A$
35	20	adantr	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to G Fn A$
36	1	adantr	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to A \in V$
37		simprl	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to k \in A$
38		fnfvof	$⊢ ((F Fn A \land G Fn A) \land (A \in V \land k \in A)) \to (F X_{f} G) (k) = F (k) X G (k)$
39	34 35 36 37 38	syl22anc	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to (F X_{f} G) (k) = F (k) X G (k)$
40		oveq12	$⊢ (F (k) = Z \land G (k) = Z) \to F (k) X G (k) = Z X Z$
41	40	ad2antll	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to F (k) X G (k) = Z X Z$
42	5	adantr	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to Z X Z = Z$
43	39 41 42	3eqtrd	$⊢ (φ \land (k \in A \land (F (k) = Z \land G (k) = Z))) \to (F X_{f} G) (k) = Z$
44	33 43	sylan2	$⊢ (φ \land (k \in A \land (\neg (k \in A \land F (k) \neq Z) \land \neg (k \in A \land G (k) \neq Z)))) \to (F X_{f} G) (k) = Z$
45	27 44	syldan	$⊢ (φ \land (k \in A \land (\neg k \in {supp}_{Z} (F) \land \neg k \in {supp}_{Z} (G)))) \to (F X_{f} G) (k) = Z$
46	14 45	sylan2b	$⊢ (φ \land k \in (A ∖ ({supp}_{Z} (F) \cup {supp}_{Z} (G)))) \to (F X_{f} G) (k) = Z$
47	8 46	suppss	$⊢ φ \to (F X_{f} G) supp Z \subseteq {supp}_{Z} (F) \cup {supp}_{Z} (G)$

Metamath Proof Explorer

Theorem suppofssd

Proof