ovnovollem1

Description: if F is a cover of B in RR , then I is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovollem1.a	$⊢ φ \to A \in V$
	ovnovollem1.f	$⊢ φ \to F \in ({ℝ^{2}}^{ℕ})$
	ovnovollem1.i	$⊢ I = (j \in ℕ ⟼ \{⟨A, F (j)⟩\})$
	ovnovollem1.s	$⊢ φ \to B \subseteq ⋃ ran ([.) \circ F)$
	ovnovollem1.b	$⊢ φ \to B \in W$
	ovnovollem1.z	$⊢ φ \to Z = sum^((vol \circ [.)) \circ F)$
Assertion	ovnovollem1	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))$

Proof

Step	Hyp	Ref	Expression
1		ovnovollem1.a	$⊢ φ \to A \in V$
2		ovnovollem1.f	$⊢ φ \to F \in ({ℝ^{2}}^{ℕ})$
3		ovnovollem1.i	$⊢ I = (j \in ℕ ⟼ \{⟨A, F (j)⟩\})$
4		ovnovollem1.s	$⊢ φ \to B \subseteq ⋃ ran ([.) \circ F)$
5		ovnovollem1.b	$⊢ φ \to B \in W$
6		ovnovollem1.z	$⊢ φ \to Z = sum^((vol \circ [.)) \circ F)$
7		eqidd	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} = \{⟨A, F (j)⟩\}$
8	1	adantr	$⊢ (φ \land j \in ℕ) \to A \in V$
9		elmapi	$⊢ F \in ({ℝ^{2}}^{ℕ}) \to F : ℕ ⟶ ℝ^{2}$
10	2 9	syl	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
11	10	ffvelrnda	$⊢ (φ \land j \in ℕ) \to F (j) \in ℝ^{2}$
12		fsng	$⊢ (A \in V \land F (j) \in ℝ^{2}) \to (\{⟨A, F (j)⟩\} : \{A\} ⟶ \{F (j)\} \leftrightarrow \{⟨A, F (j)⟩\} = \{⟨A, F (j)⟩\})$
13	8 11 12	syl2anc	$⊢ (φ \land j \in ℕ) \to (\{⟨A, F (j)⟩\} : \{A\} ⟶ \{F (j)\} \leftrightarrow \{⟨A, F (j)⟩\} = \{⟨A, F (j)⟩\})$
14	7 13	mpbird	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} : \{A\} ⟶ \{F (j)\}$
15	11	snssd	$⊢ (φ \land j \in ℕ) \to \{F (j)\} \subseteq ℝ^{2}$
16	14 15	fssd	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} : \{A\} ⟶ ℝ^{2}$
17		reex	$⊢ ℝ \in V$
18	17 17	xpex	$⊢ ℝ^{2} \in V$
19	18	a1i	$⊢ (φ \land j \in ℕ) \to ℝ^{2} \in V$
20		snex	$⊢ \{A\} \in V$
21	20	a1i	$⊢ (φ \land j \in ℕ) \to \{A\} \in V$
22	19 21	elmapd	$⊢ (φ \land j \in ℕ) \to (\{⟨A, F (j)⟩\} \in ({ℝ^{2}}^{\{A\}}) \leftrightarrow \{⟨A, F (j)⟩\} : \{A\} ⟶ ℝ^{2})$
23	16 22	mpbird	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} \in ({ℝ^{2}}^{\{A\}})$
24	23 3	fmptd	$⊢ φ \to I : ℕ ⟶ {ℝ^{2}}^{\{A\}}$
25		ovexd	$⊢ φ \to {ℝ^{2}}^{\{A\}} \in V$
26		nnex	$⊢ ℕ \in V$
27	26	a1i	$⊢ φ \to ℕ \in V$
28	25 27	elmapd	$⊢ φ \to (I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \leftrightarrow I : ℕ ⟶ {ℝ^{2}}^{\{A\}})$
29	24 28	mpbird	$⊢ φ \to I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ})$
30		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
31	30	a1i	$⊢ φ \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
32		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
33	32	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
34	31 33 10	fcoss	$⊢ φ \to ([.) \circ F) : ℕ ⟶ 𝒫 ℝ^{*}$
35	34	ffnd	$⊢ φ \to ([.) \circ F) Fn ℕ$
36		fniunfv	$⊢ ([.) \circ F) Fn ℕ \to ⋃_{j \in ℕ} ([.) \circ F) (j) = ⋃ ran ([.) \circ F)$
37	35 36	syl	$⊢ φ \to ⋃_{j \in ℕ} ([.) \circ F) (j) = ⋃ ran ([.) \circ F)$
38	37	eqcomd	$⊢ φ \to ⋃ ran ([.) \circ F) = ⋃_{j \in ℕ} ([.) \circ F) (j)$
39	4 38	sseqtrd	$⊢ φ \to B \subseteq ⋃_{j \in ℕ} ([.) \circ F) (j)$
40		fvex	$⊢ ([.) \circ F) (j) \in V$
41	26 40	iunex	$⊢ ⋃_{j \in ℕ} ([.) \circ F) (j) \in V$
42	41	a1i	$⊢ φ \to ⋃_{j \in ℕ} ([.) \circ F) (j) \in V$
43	20	a1i	$⊢ φ \to \{A\} \in V$
44	1	snn0d	$⊢ φ \to \{A\} \neq \emptyset$
45	5 42 43 44	mapss2	$⊢ φ \to (B \subseteq ⋃_{j \in ℕ} ([.) \circ F) (j) \leftrightarrow B^{\{A\}} \subseteq {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}})$
46	39 45	mpbid	$⊢ φ \to B^{\{A\}} \subseteq {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}}$
47		nfv	$⊢ Ⅎ j φ$
48		fvexd	$⊢ (φ \land j \in ℕ) \to [.) (F (j)) \in V$
49	47 27 48 1	iunmapsn	$⊢ φ \to ⋃_{j \in ℕ} ({[.) (F (j))}^{\{A\}}) = {⋃_{j \in ℕ} [.) (F (j))}^{\{A\}}$
50	49	eqcomd	$⊢ φ \to {⋃_{j \in ℕ} [.) (F (j))}^{\{A\}} = ⋃_{j \in ℕ} ({[.) (F (j))}^{\{A\}})$
51		elmapfun	$⊢ F \in ({ℝ^{2}}^{ℕ}) \to Fun F$
52	2 51	syl	$⊢ φ \to Fun F$
53	52	adantr	$⊢ (φ \land j \in ℕ) \to Fun F$
54		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
55	10	fdmd	$⊢ φ \to dom F = ℕ$
56	55	eqcomd	$⊢ φ \to ℕ = dom F$
57	56	adantr	$⊢ (φ \land j \in ℕ) \to ℕ = dom F$
58	54 57	eleqtrd	$⊢ (φ \land j \in ℕ) \to j \in dom F$
59		fvco	$⊢ (Fun F \land j \in dom F) \to ([.) \circ F) (j) = [.) (F (j))$
60	53 58 59	syl2anc	$⊢ (φ \land j \in ℕ) \to ([.) \circ F) (j) = [.) (F (j))$
61	60	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} ([.) \circ F) (j) = ⋃_{j \in ℕ} [.) (F (j))$
62	61	oveq1d	$⊢ φ \to {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}} = {⋃_{j \in ℕ} [.) (F (j))}^{\{A\}}$
63	14	ffund	$⊢ (φ \land j \in ℕ) \to Fun \{⟨A, F (j)⟩\}$
64		id	$⊢ j \in ℕ \to j \in ℕ$
65		snex	$⊢ \{⟨A, F (j)⟩\} \in V$
66	65	a1i	$⊢ j \in ℕ \to \{⟨A, F (j)⟩\} \in V$
67	3	fvmpt2	$⊢ (j \in ℕ \land \{⟨A, F (j)⟩\} \in V) \to I (j) = \{⟨A, F (j)⟩\}$
68	64 66 67	syl2anc	$⊢ j \in ℕ \to I (j) = \{⟨A, F (j)⟩\}$
69	68	adantl	$⊢ (φ \land j \in ℕ) \to I (j) = \{⟨A, F (j)⟩\}$
70	69	funeqd	$⊢ (φ \land j \in ℕ) \to (Fun I (j) \leftrightarrow Fun \{⟨A, F (j)⟩\})$
71	63 70	mpbird	$⊢ (φ \land j \in ℕ) \to Fun I (j)$
72	71	adantr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to Fun I (j)$
73		simpr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to k \in \{A\}$
74	69	dmeqd	$⊢ (φ \land j \in ℕ) \to dom I (j) = dom \{⟨A, F (j)⟩\}$
75	14	fdmd	$⊢ (φ \land j \in ℕ) \to dom \{⟨A, F (j)⟩\} = \{A\}$
76	74 75	eqtrd	$⊢ (φ \land j \in ℕ) \to dom I (j) = \{A\}$
77	76	eleq2d	$⊢ (φ \land j \in ℕ) \to (k \in dom I (j) \leftrightarrow k \in \{A\})$
78	77	adantr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to (k \in dom I (j) \leftrightarrow k \in \{A\})$
79	73 78	mpbird	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to k \in dom I (j)$
80		fvco	$⊢ (Fun I (j) \land k \in dom I (j)) \to ([.) \circ I (j)) (k) = [.) (I (j) (k))$
81	72 79 80	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to ([.) \circ I (j)) (k) = [.) (I (j) (k))$
82	68	fveq1d	$⊢ j \in ℕ \to I (j) (k) = \{⟨A, F (j)⟩\} (k)$
83	82	ad2antlr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to I (j) (k) = \{⟨A, F (j)⟩\} (k)$
84		elsni	$⊢ k \in \{A\} \to k = A$
85	84	fveq2d	$⊢ k \in \{A\} \to \{⟨A, F (j)⟩\} (k) = \{⟨A, F (j)⟩\} (A)$
86	85	adantl	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to \{⟨A, F (j)⟩\} (k) = \{⟨A, F (j)⟩\} (A)$
87		fvexd	$⊢ φ \to F (j) \in V$
88		fvsng	$⊢ (A \in V \land F (j) \in V) \to \{⟨A, F (j)⟩\} (A) = F (j)$
89	1 87 88	syl2anc	$⊢ φ \to \{⟨A, F (j)⟩\} (A) = F (j)$
90	89	ad2antrr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to \{⟨A, F (j)⟩\} (A) = F (j)$
91	83 86 90	3eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to I (j) (k) = F (j)$
92	91	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to [.) (I (j) (k)) = [.) (F (j))$
93		eqidd	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to [.) (F (j)) = [.) (F (j))$
94	81 92 93	3eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to ([.) \circ I (j)) (k) = [.) (F (j))$
95	94	ixpeq2dva	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = \underset{k \in \{A\}}{⨉} [.) (F (j))$
96		fvex	$⊢ [.) (F (j)) \in V$
97	20 96	ixpconst	$⊢ \underset{k \in \{A\}}{⨉} [.) (F (j)) = {[.) (F (j))}^{\{A\}}$
98	97	a1i	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} [.) (F (j)) = {[.) (F (j))}^{\{A\}}$
99	95 98	eqtrd	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = {[.) (F (j))}^{\{A\}}$
100	99	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = ⋃_{j \in ℕ} ({[.) (F (j))}^{\{A\}})$
101	50 62 100	3eqtr4d	$⊢ φ \to {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}} = ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
102	46 101	sseqtrd	$⊢ φ \to B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
103		nfcv	$⊢ \underline{Ⅎ} j F$
104		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
105		xpss2	$⊢ ℝ \subseteq ℝ^{} \to ℝ^{2} \subseteq ℝ \times ℝ^{}$
106	104 105	ax-mp	$⊢ ℝ^{2} \subseteq ℝ \times ℝ^{*}$
107	106	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ \times ℝ^{*}$
108	10 107	fssd	$⊢ φ \to F : ℕ ⟶ ℝ \times ℝ^{*}$
109	103 108	volicofmpt	$⊢ φ \to (vol \circ [.)) \circ F = (j \in ℕ ⟼ vol ([1^{st} (F (j)), 2^{nd} (F (j)))))$
110	68	coeq2d	$⊢ j \in ℕ \to [.) \circ I (j) = [.) \circ \{⟨A, F (j)⟩\}$
111	110	fveq1d	$⊢ j \in ℕ \to ([.) \circ I (j)) (A) = ([.) \circ \{⟨A, F (j)⟩\}) (A)$
112	111	adantl	$⊢ (φ \land j \in ℕ) \to ([.) \circ I (j)) (A) = ([.) \circ \{⟨A, F (j)⟩\}) (A)$
113		snidg	$⊢ A \in V \to A \in \{A\}$
114	1 113	syl	$⊢ φ \to A \in \{A\}$
115		dmsnopg	$⊢ F (j) \in V \to dom \{⟨A, F (j)⟩\} = \{A\}$
116	87 115	syl	$⊢ φ \to dom \{⟨A, F (j)⟩\} = \{A\}$
117	114 116	eleqtrrd	$⊢ φ \to A \in dom \{⟨A, F (j)⟩\}$
118	117	adantr	$⊢ (φ \land j \in ℕ) \to A \in dom \{⟨A, F (j)⟩\}$
119		fvco	$⊢ (Fun \{⟨A, F (j)⟩\} \land A \in dom \{⟨A, F (j)⟩\}) \to ([.) \circ \{⟨A, F (j)⟩\}) (A) = [.) (\{⟨A, F (j)⟩\} (A))$
120	63 118 119	syl2anc	$⊢ (φ \land j \in ℕ) \to ([.) \circ \{⟨A, F (j)⟩\}) (A) = [.) (\{⟨A, F (j)⟩\} (A))$
121		fvexd	$⊢ (φ \land j \in ℕ) \to F (j) \in V$
122	8 121 88	syl2anc	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} (A) = F (j)$
123		1st2nd2	$⊢ F (j) \in ℝ^{2} \to F (j) = ⟨1^{st} (F (j)), 2^{nd} (F (j))⟩$
124	11 123	syl	$⊢ (φ \land j \in ℕ) \to F (j) = ⟨1^{st} (F (j)), 2^{nd} (F (j))⟩$
125	122 124	eqtrd	$⊢ (φ \land j \in ℕ) \to \{⟨A, F (j)⟩\} (A) = ⟨1^{st} (F (j)), 2^{nd} (F (j))⟩$
126	125	fveq2d	$⊢ (φ \land j \in ℕ) \to [.) (\{⟨A, F (j)⟩\} (A)) = [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩)$
127		df-ov	$⊢ [1^{st} (F (j)), 2^{nd} (F (j))) = [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩)$
128	127	eqcomi	$⊢ [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩) = [1^{st} (F (j)), 2^{nd} (F (j)))$
129	128	a1i	$⊢ (φ \land j \in ℕ) \to [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩) = [1^{st} (F (j)), 2^{nd} (F (j)))$
130	126 129	eqtrd	$⊢ (φ \land j \in ℕ) \to [.) (\{⟨A, F (j)⟩\} (A)) = [1^{st} (F (j)), 2^{nd} (F (j)))$
131	112 120 130	3eqtrd	$⊢ (φ \land j \in ℕ) \to ([.) \circ I (j)) (A) = [1^{st} (F (j)), 2^{nd} (F (j)))$
132	131	fveq2d	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) = vol ([1^{st} (F (j)), 2^{nd} (F (j))))$
133		xp1st	$⊢ F (j) \in ℝ^{2} \to 1^{st} (F (j)) \in ℝ$
134	11 133	syl	$⊢ (φ \land j \in ℕ) \to 1^{st} (F (j)) \in ℝ$
135		xp2nd	$⊢ F (j) \in ℝ^{2} \to 2^{nd} (F (j)) \in ℝ$
136	11 135	syl	$⊢ (φ \land j \in ℕ) \to 2^{nd} (F (j)) \in ℝ$
137		volicore	$⊢ (1^{st} (F (j)) \in ℝ \land 2^{nd} (F (j)) \in ℝ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) \in ℝ$
138	134 136 137	syl2anc	$⊢ (φ \land j \in ℕ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) \in ℝ$
139	132 138	eqeltrd	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) \in ℝ$
140	139	recnd	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) \in ℂ$
141		2fveq3	$⊢ k = A \to vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
142	141	prodsn	$⊢ (A \in V \land vol (([.) \circ I (j)) (A)) \in ℂ) \to \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
143	8 140 142	syl2anc	$⊢ (φ \land j \in ℕ) \to \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
144	143 132	eqtr2d	$⊢ (φ \land j \in ℕ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) = \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))$
145	144	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ vol ([1^{st} (F (j)), 2^{nd} (F (j))))) = (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))$
146	109 145	eqtrd	$⊢ φ \to (vol \circ [.)) \circ F = (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))$
147	146	fveq2d	$⊢ φ \to sum^((vol \circ [.)) \circ F) = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
148	6 147	eqtrd	$⊢ φ \to Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
149	102 148	jca	$⊢ φ \to (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))))$
150		fveq1	$⊢ i = I \to i (j) = I (j)$
151	150	coeq2d	$⊢ i = I \to [.) \circ i (j) = [.) \circ I (j)$
152	151	fveq1d	$⊢ i = I \to ([.) \circ i (j)) (k) = ([.) \circ I (j)) (k)$
153	152	ixpeq2dv	$⊢ i = I \to \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) = \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
154	153	iuneq2d	$⊢ i = I \to ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
155	154	sseq2d	$⊢ i = I \to (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \leftrightarrow B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k))$
156		simpl	$⊢ (i = I \land k \in \{A\}) \to i = I$
157	156	fveq1d	$⊢ (i = I \land k \in \{A\}) \to i (j) = I (j)$
158	157	coeq2d	$⊢ (i = I \land k \in \{A\}) \to [.) \circ i (j) = [.) \circ I (j)$
159	158	fveq1d	$⊢ (i = I \land k \in \{A\}) \to ([.) \circ i (j)) (k) = ([.) \circ I (j)) (k)$
160	159	fveq2d	$⊢ (i = I \land k \in \{A\}) \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ I (j)) (k))$
161	160	prodeq2dv	$⊢ i = I \to \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)) = \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))$
162	161	mpteq2dv	$⊢ i = I \to (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))$
163	162	fveq2d	$⊢ i = I \to sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
164	163	eqeq2d	$⊢ i = I \to (Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))) \leftrightarrow Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))))$
165	155 164	anbi12d	$⊢ i = I \to ((B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))) \leftrightarrow (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))))$
166	165	rspcev	$⊢ (I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))))) \to \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))$
167	29 149 166	syl2anc	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))$

Metamath Proof Explorer

Theorem ovnovollem1

Proof