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	bilani	$⊢ (φ \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⟩$
45	42 44	r19.29vva	$⊢ (φ \land z \in ((A ∖ {supp}_{(B \times \{Z\})} (G)) \times B)) \to F (z) = Z$
46	45	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$
47		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⟩$
48	47	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⟩)$
49		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$
50		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)))$
51	50	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$
52		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 φ$
53	52 49 51 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$
54	49 51 53 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$
55	12 54	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$
56	52 49 51 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$
57		fvexd	$⊢ ((φ \land x \in A) \land y \in B) \to G (x) (y) \in V$
58	34 33 57	fmpt2d	$⊢ (φ \land x \in A) \to G (x) : B ⟶ V$
59		ssiun2	$⊢ x \in A \to G (x) supp Z \subseteq ⋃_{x \in A} {supp}_{Z} (G (x))$
60	59	adantl	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{x \in A} {supp}_{Z} (G (x))$
61		fveq2	$⊢ x = k \to G (x) = G (k)$
62	61	oveq1d	$⊢ x = k \to G (x) supp Z = G (k) supp Z$
63	62	cbviunv	$⊢ ⋃_{x \in A} {supp}_{Z} (G (x)) = ⋃_{k \in A} {supp}_{Z} (G (k))$
64	60 63	sseqtrdi	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{k \in A} {supp}_{Z} (G (k))$
65		simpl	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to φ$
66		simpr	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to k \in (A ∖ {supp}_{(B \times \{Z\})} (G))$
67	66	eldifad	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to k \in A$
68	23 24 3 27	suppssr	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (k) = B \times \{Z\}$
69		eleq1w	$⊢ x = k \to (x \in A \leftrightarrow k \in A)$
70	69	anbi2d	$⊢ x = k \to ((φ \land x \in A) \leftrightarrow (φ \land k \in A))$
71	61	fneq1d	$⊢ x = k \to (G (x) Fn B \leftrightarrow G (k) Fn B)$
72	70 71	imbi12d	$⊢ x = k \to (((φ \land x \in A) \to G (x) Fn B) \leftrightarrow ((φ \land k \in A) \to G (k) Fn B))$
73	58	ffnd	$⊢ (φ \land x \in A) \to G (x) Fn B$
74	72 73	chvarvv	$⊢ (φ \land k \in A) \to G (k) Fn B$
75	4	adantr	$⊢ (φ \land k \in A) \to B \in W$
76	5	adantr	$⊢ (φ \land k \in A) \to Z \in D$
77		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\})$
78	74 75 76 77	syl3anc	$⊢ (φ \land k \in A) \to (G (k) supp Z = \emptyset \leftrightarrow G (k) = B \times \{Z\})$
79	78	biimpar	$⊢ ((φ \land k \in A) \land G (k) = B \times \{Z\}) \to G (k) supp Z = \emptyset$
80	65 67 68 79	syl21anc	$⊢ (φ \land k \in (A ∖ {supp}_{(B \times \{Z\})} (G))) \to G (k) supp Z = \emptyset$
81	80	ralrimiva	$⊢ φ \to \forall k \in (A ∖ {supp}_{(B \times \{Z\})} (G)) G (k) supp Z = \emptyset$
82		nfcv	$⊢ \underline{Ⅎ} k (A ∖ {supp}_{(B \times \{Z\})} (G))$
83	82	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))$
84	81 83	syl	$⊢ φ \to ⋃_{k \in A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))} {supp}_{Z} (G (k)) = ⋃_{k \in A} {supp}_{Z} (G (k))$
85		dfin4	$⊢ A \cap {supp}_{(B \times \{Z\})} (G) = A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G))$
86		suppssdm	$⊢ G supp (B \times \{Z\}) \subseteq dom G$
87	86 23	fssdm	$⊢ φ \to G supp (B \times \{Z\}) \subseteq A$
88		sseqin2	$⊢ G supp (B \times \{Z\}) \subseteq A \leftrightarrow A \cap {supp}_{(B \times \{Z\})} (G) = G supp (B \times \{Z\})$
89	87 88	sylib	$⊢ φ \to A \cap {supp}_{(B \times \{Z\})} (G) = G supp (B \times \{Z\})$
90	85 89	eqtr3id	$⊢ φ \to A ∖ (A ∖ {supp}_{(B \times \{Z\})} (G)) = G supp (B \times \{Z\})$
91	90	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))$
92	84 91	eqtr3d	$⊢ φ \to ⋃_{k \in A} {supp}_{Z} (G (k)) = ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
93	92	adantr	$⊢ (φ \land x \in A) \to ⋃_{k \in A} {supp}_{Z} (G (k)) = ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
94	64 93	sseqtrd	$⊢ (φ \land x \in A) \to G (x) supp Z \subseteq ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))$
95	5	adantr	$⊢ (φ \land x \in A) \to Z \in D$
96	58 94 21 95	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$
97	96	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$
98	56 97	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$
99	48 55 98	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$
100	99	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$
101		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⟩$
102	101	bilani	$⊢ (φ \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⟩$
103	100 102	r19.29vva	$⊢ (φ \land z \in (A \times (B ∖ ⋃_{k \in G supp (B \times \{Z\})} {supp}_{Z} (G (k))))) \to F (z) = Z$
104	103	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$
105		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))))$
106		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))))$
107	105 106	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)))))$
108		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)))))$
109	107 108	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)))))$
110	46 104 109	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$
111	9 110	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