suppovss

Description: A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023)

	Ref	Expression
Hypotheses	suppovss.f	$⊢ F = (x \in A, y \in B ⟼ C)$
	suppovss.g	$⊢ G = (x \in A ⟼ (y \in B ⟼ C))$
	suppovss.a	$⊢ φ \to A \in V$
	suppovss.b	$⊢ φ \to B \in W$
	suppovss.z	$⊢ φ \to Z \in D$
	suppovss.1	$⊢ (φ \land (x \in A \land y \in B)) \to C \in D$
Assertion	suppovss	$⊢ φ \to F supp Z \subseteq {supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$

Proof

Step	Hyp	Ref	Expression
1		suppovss.f	$⊢ F = (x \in A, y \in B ⟼ C)$
2		suppovss.g	$⊢ G = (x \in A ⟼ (y \in B ⟼ C))$
3		suppovss.a	$⊢ φ \to A \in V$
4		suppovss.b	$⊢ φ \to B \in W$
5		suppovss.z	$⊢ φ \to Z \in D$
6		suppovss.1	$⊢ (φ \land (x \in A \land y \in B)) \to C \in D$
7	6	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in B C \in D$
8	1	fmpo	$⊢ \forall x \in A \forall y \in B C \in D \leftrightarrow F : A \times B ⟶ D$
9	7 8	sylib	$⊢ φ \to F : A \times B ⟶ D$
10		simpr	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to z = ⟨x, y⟩$
11	10	fveq2d	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to F (z) = F (⟨x, y⟩)$
12		df-ov	$⊢ x F y = F (⟨x, y⟩)$
13		simpllr	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to x \in (A ∖ {supp}_{(B \times \{Z\})} (G))$
14	13	eldifad	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to x \in A$
15		simplr	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to y \in B$
16		simplll	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to φ$
17	16 14 15 6	syl12anc	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to C \in D$
18	1	ovmpt4g	$⊢ (x \in A \land y \in B \land C \in D) \to x F y = C$
19	14 15 17 18	syl3anc	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to x F y = C$
20	12 19	eqtr3id	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to F (⟨x, y⟩) = C$
21	4	adantr	$⊢ (φ \land x \in A) \to B \in W$
22	21	mptexd	$⊢ (φ \land x \in A) \to (y \in B ⟼ C) \in V$
23	22 2	fmptd	$⊢ φ \to G : A ⟶ V$
24		ssidd	$⊢ φ \to G supp (B \times \{Z\}) \subseteq G supp (B \times \{Z\})$
25		snex	$⊢ \{Z\} \in V$
26	25	a1i	$⊢ φ \to \{Z\} \in V$
27	4 26	xpexd	$⊢ φ \to B \times \{Z\} \in V$
28	23 24 3 27	suppssr	$⊢ (φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (x) = B \times \{Z\}$
29	28	fveq1d	$⊢ (φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (x) (y) = (B \times \{Z\}) (y)$
30	16 13 29	syl2anc	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to G (x) (y) = (B \times \{Z\}) (y)$
31		simpr	$⊢ (φ \land x \in A) \to x \in A$
32	2	fvmpt2	$⊢ (x \in A \land (y \in B ⟼ C) \in V) \to G (x) = (y \in B ⟼ C)$
33	31 22 32	syl2anc	$⊢ (φ \land x \in A) \to G (x) = (y \in B ⟼ C)$
34	6	anassrs	$⊢ ((φ \land x \in A) \land y \in B) \to C \in D$
35	33 34	fvmpt2d	$⊢ ((φ \land x \in A) \land y \in B) \to G (x) (y) = C$
36	16 14 15 35	syl21anc	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to G (x) (y) = C$
37	16 5	syl	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to Z \in D$
38		fvconst2g	$⊢ (Z \in D \land y \in B) \to (B \times \{Z\}) (y) = Z$
39	37 15 38	syl2anc	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to (B \times \{Z\}) (y) = Z$
40	30 36 39	3eqtr3d	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to C = Z$
41	11 20 40	3eqtrd	$⊢ (((φ \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to F (z) = Z$
42	41	adantl3r	$⊢ ((((φ \land z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B)) \land x \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \land y \in B) \land z = ⟨x, y⟩) \to F (z) = Z$
43		elxp2	$⊢ z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \leftrightarrow \exists x \in (A ∖ {supp}_{(B \times \{Z\})} (G)) \exists y \in B z = ⟨x, y⟩$
44	43	biimpi	$⊢ z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \to \exists x \in (A ∖ {supp}_{(B \times \{Z\})} (G)) \exists y \in B z = ⟨x, y⟩$
45	44	adantl	$⊢ (φ \land z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B)) \to \exists x \in (A ∖ {supp}_{(B \times \{Z\})} (G)) \exists y \in B z = ⟨x, y⟩$
46	42 45	r19.29vva	$⊢ (φ \land z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B)) \to F (z) = Z$
47	46	adantlr	$⊢ ((φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \land z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B)) \to F (z) = Z$
48		simpr	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to z = ⟨x, y⟩$
49	48	fveq2d	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to F (z) = F (⟨x, y⟩)$
50		simpllr	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to x \in A$
51		simplr	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))$
52	51	eldifad	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to y \in B$
53		simplll	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to φ$
54	53 50 52 6	syl12anc	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to C \in D$
55	50 52 54 18	syl3anc	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to x F y = C$
56	12 55	eqtr3id	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to F (⟨x, y⟩) = C$
57	53 50 52 35	syl21anc	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to G (x) (y) = C$
58		fvexd	$⊢ ((φ \land x \in A) \land y \in B) \to G (x) (y) \in V$
59	34 33 58	fmpt2d	$⊢ (φ \land x \in A) \to G (x) : B ⟶ V$
60		ssiun2	$⊢ x \in A \to G (x) supp Z \subseteq ⋃_{x \in A} {supp}_{Z} (G (x))$
61	60	adantl	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{x \in A} {supp}_{Z} (G (x))$
62		fveq2	$⊢ x = k \to G (x) = G (k)$
63	62	oveq1d	$⊢ x = k \to G (x) supp Z = G (k) supp Z$
64	63	cbviunv	$⊢ ⋃_{x \in A} {supp}_{Z} (G (x)) = ⋃_{k \in A} {supp}_{Z} (G (k))$
65	61 64	sseqtrdi	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{k \in A} {supp}_{Z} (G (k))$
66		simpl	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to φ$
67		simpr	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to k \in (A ∖ {supp}_{(B \times \{Z\})} (G))$
68	67	eldifad	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to k \in A$
69	23 24 3 27	suppssr	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (k) = B \times \{Z\}$
70		eleq1w	$⊢ x = k \to (x \in A \leftrightarrow k \in A)$
71	70	anbi2d	$⊢ x = k \to ((φ \land x \in A) \leftrightarrow (φ \land k \in A))$
72	62	fneq1d	$⊢ x = k \to (G (x) Fn B \leftrightarrow G (k) Fn B)$
73	71 72	imbi12d	$⊢ x = k \to (((φ \land x \in A) \to G (x) Fn B) \leftrightarrow ((φ \land k \in A) \to G (k) Fn B))$
74	59	ffnd	$⊢ (φ \land x \in A) \to G (x) Fn B$
75	73 74	chvarvv	$⊢ (φ \land k \in A) \to G (k) Fn B$
76	4	adantr	$⊢ (φ \land k \in A) \to B \in W$
77	5	adantr	$⊢ (φ \land k \in A) \to Z \in D$
78		fnsuppeq0	$⊢ (G (k) Fn B \land B \in W \land Z \in D) \to (G (k) supp Z = \emptyset \leftrightarrow G (k) = B \times \{Z\})$
79	75 76 77 78	syl3anc	$⊢ (φ \land k \in A) \to (G (k) supp Z = \emptyset \leftrightarrow G (k) = B \times \{Z\})$
80	79	biimpar	$⊢ ((φ \land k \in A) \land G (k) = B \times \{Z\}) \to G (k) supp Z = \emptyset$
81	66 68 69 80	syl21anc	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (k) supp Z = \emptyset$
82	81	ralrimiva	$⊢ φ \to \forall k \in (A ∖ {supp}_{(B \times \{Z\})} (G)) G (k) supp Z = \emptyset$
83		nfcv	$⊢ \underline{Ⅎ} k (A ∖ {supp}_{(B \times \{Z\})} (G))$
84	83	iunxdif3	$⊢ \forall k \in (A ∖ {supp}_{(B \times \{Z\})} (G)) G (k) supp Z = \emptyset \to ⋃_{k \in A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))} {supp}_{Z} (G (k)) = ⋃_{k \in A} {supp}_{Z} (G (k))$
85	82 84	syl	$⊢ φ \to ⋃_{k \in A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))} {supp}_{Z} (G (k)) = ⋃_{k \in A} {supp}_{Z} (G (k))$
86		dfin4	$⊢ A \cap {supp}_{(B \times \{Z\})} (G) = A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))$
87		suppssdm	$⊢ G supp (B \times \{Z\}) \subseteq dom G$
88	87 23	fssdm	$⊢ φ \to G supp (B \times \{Z\}) \subseteq A$
89		sseqin2	$⊢ G supp (B \times \{Z\}) \subseteq A \leftrightarrow A \cap {supp}_{(B \times \{Z\})} (G) = G supp (B \times \{Z\})$
90	88 89	sylib	$⊢ φ \to A \cap {supp}_{(B \times \{Z\})} (G) = G supp (B \times \{Z\})$
91	86 90	eqtr3id	$⊢ φ \to A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G)) = G supp (B \times \{Z\})$
92	91	iuneq1d	$⊢ φ \to ⋃_{k \in A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))} {supp}_{Z} (G (k)) = ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
93	85 92	eqtr3d	$⊢ φ \to ⋃_{k \in A} {supp}_{Z} (G (k)) = ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
94	93	adantr	$⊢ (φ \land x \in A) \to ⋃_{k \in A} {supp}_{Z} (G (k)) = ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
95	65 94	sseqtrd	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
96	5	adantr	$⊢ (φ \land x \in A) \to Z \in D$
97	59 95 21 96	suppssr	$⊢ ((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \to G (x) (y) = Z$
98	97	adantr	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to G (x) (y) = Z$
99	57 98	eqtr3d	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to C = Z$
100	49 56 99	3eqtrd	$⊢ (((φ \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to F (z) = Z$
101	100	adantl3r	$⊢ ((((φ \land z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \land x \in A) \land y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \land z = ⟨x, y⟩) \to F (z) = Z$
102		elxp2	$⊢ z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \leftrightarrow \exists x \in A \exists y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))) z = ⟨x, y⟩$
103	102	biimpi	$⊢ z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))) \to \exists x \in A \exists y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))) z = ⟨x, y⟩$
104	103	adantl	$⊢ (φ \land z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to \exists x \in A \exists y \in (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))) z = ⟨x, y⟩$
105	101 104	r19.29vva	$⊢ (φ \land z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to F (z) = Z$
106	105	adantlr	$⊢ ((φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \land z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to F (z) = Z$
107		simpr	$⊢ (φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))$
108		difxp	$⊢ (A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))) = ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \cup (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))$
109	107 108	eleqtrdi	$⊢ (φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to z \in (((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \cup (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))))$
110		elun	$⊢ z \in (((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \cup (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \leftrightarrow (z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \lor z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))))$
111	109 110	sylib	$⊢ (φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to (z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B) \lor z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k)))))$
112	47 106 111	mpjaodan	$⊢ (φ \land z \in ((A \times B) ∖ ({supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to F (z) = Z$
113	9 112	suppss	$⊢ φ \to F supp Z \subseteq {supp}_{(B \times \{Z\})} (G) \times ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$

Metamath Proof Explorer

Theorem suppovss

Proof