Theorem ovnovollem2 47499

Description: if 𝐼 is a cover of (𝐵 ↑_m {𝐴}) in ℝ^1, then 𝐹 is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
ovnovollem2.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
ovnovollem2.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
ovnovollem2.i	⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
ovnovollem2.s	⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
ovnovollem2.z	⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
ovnovollem2.f	⊢ 𝐹 = (𝑗 ∈ ℕ ↦ ((𝐼‘𝑗)‘𝐴))

Assertion

Ref	Expression
ovnovollem2	⊢ (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))

Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑓   𝑓,𝐹   𝑗,𝐹,𝑘   𝑘,𝐼   𝑘,𝑉   𝑓,𝑍   𝜑,𝑗,𝑘

Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑗, 𝑘)   𝐼(𝑓, 𝑗)   𝑉(𝑓, 𝑗)   𝑊(𝑓, 𝑗, 𝑘)   𝑍(𝑗, 𝑘)

Proof of Theorem ovnovollem2

Step	Hyp	Ref	Expression
1		ovnovollem2.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
2		elmapi 8852	. . . . . . . . 9 ⊢ (𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
3	1, 2	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
4	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
5		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
6	4, 5	ffvelcdmd 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) ∈ ((ℝ × ℝ) ↑m {𝐴}))
7		elmapi 8852	. . . . . 6 ⊢ ((𝐼‘𝑗) ∈ ((ℝ × ℝ) ↑m {𝐴}) → (𝐼‘𝑗):{𝐴}⟶(ℝ × ℝ))
8	6, 7	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗):{𝐴}⟶(ℝ × ℝ))
9		ovnovollem2.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
10		snidg 4621	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
11	9, 10	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
12	11	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ {𝐴})
13	8, 12	ffvelcdmd 7080	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑗)‘𝐴) ∈ (ℝ × ℝ))
14		ovnovollem2.f	. . . 4 ⊢ 𝐹 = (𝑗 ∈ ℕ ↦ ((𝐼‘𝑗)‘𝐴))
15	13, 14	fmptd 7109	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
16		reex 11237	. . . . . 6 ⊢ ℝ ∈ V
17	16, 16	xpex 7754	. . . . 5 ⊢ (ℝ × ℝ) ∈ V
18		nnex 12285	. . . . 5 ⊢ ℕ ∈ V
19	17, 18	elmap 8882	. . . 4 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) ↔ 𝐹:ℕ⟶(ℝ × ℝ))
20	19	a1i 11	. . 3 ⊢ (𝜑 → (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) ↔ 𝐹:ℕ⟶(ℝ × ℝ)))
21	15, 20	mpbird 260	. 2 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ))
22		ovnovollem2.s	. . . . . 6 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
23		elsni 4601	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
24	23	fveq2d 6884	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝐴))
25	24	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝐴))
26		elmapfun 8871	. . . . . . . . . . . . . 14 ⊢ ((𝐼‘𝑗) ∈ ((ℝ × ℝ) ↑m {𝐴}) → Fun (𝐼‘𝑗))
27	6, 26	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗))
28	8	fdmd 6715	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
29	28	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} = dom (𝐼‘𝑗))
30	12, 29	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom (𝐼‘𝑗))
31		fvco 6978	. . . . . . . . . . . . 13 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝐴 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ([,)‘((𝐼‘𝑗)‘𝐴)))
32	27, 30, 31	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ([,)‘((𝐼‘𝑗)‘𝐴)))
33	32	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ([,)‘((𝐼‘𝑗)‘𝐴)))
34		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
35		fvexd 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝐴) ∈ V)
36	14	fvmpt2 7000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℕ ∧ ((𝐼‘𝑗)‘𝐴) ∈ V) → (𝐹‘𝑗) = ((𝐼‘𝑗)‘𝐴))
37	34, 35, 36	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = ((𝐼‘𝑗)‘𝐴))
38	37	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝐴) = (𝐹‘𝑗))
39	38	fveq2d 6884	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ([,)‘((𝐼‘𝑗)‘𝐴)) = ([,)‘(𝐹‘𝑗)))
40	39	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘((𝐼‘𝑗)‘𝐴)) = ([,)‘(𝐹‘𝑗)))
41	15	ffund 6709	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Fun 𝐹)
42	41	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
43	14, 13	dmmptd 6679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝐹 = ℕ)
44	43	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ = dom 𝐹)
45	44	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
46	5, 45	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
47		fvco 6978	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
48	42, 46, 47	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
49	48	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) = (([,) ∘ 𝐹)‘𝑗))
50	40, 49	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘((𝐼‘𝑗)‘𝐴)) = (([,) ∘ 𝐹)‘𝑗))
51	50	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝐴)) = (([,) ∘ 𝐹)‘𝑗))
52	25, 33, 51	3eqtrd 2799	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,) ∘ 𝐹)‘𝑗))
53	52	ixpeq2dva 8923	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ 𝐹)‘𝑗))
54		snex 5404	. . . . . . . . . . 11 ⊢ {𝐴} ∈ V
55		fvex 6893	. . . . . . . . . . 11 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
56	54, 55	ixpconst 8918	. . . . . . . . . 10 ⊢ X𝑘 ∈ {𝐴} (([,) ∘ 𝐹)‘𝑗) = ((([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})
57	56	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ 𝐹)‘𝑗) = ((([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
58	53, 57	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ((([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
59	58	iuneq2dv 4976	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ ((([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
60		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑗𝜑
61	18	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ ∈ V)
62		fvexd 6895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) ∈ V)
63	60, 61, 62, 9	iunmapsn 46061	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ ((([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
64	59, 63	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
65	22, 64	sseqtrd 3967	. . . . 5 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
66		ovnovollem2.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
67	18, 55	iunex 7967	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
68	67	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
69	54	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
70	11	ne0d 4288	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
71	66, 68, 69, 70	mapss2 46050	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})))
72	65, 71	mpbird 260	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
73		icof 46063	. . . . . . . 8 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
74	73	a1i 11	. . . . . . 7 ⊢ (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
75		rexpssxrxp 11300	. . . . . . . 8 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
76	75	a1i 11	. . . . . . 7 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
77	74, 76, 15	fcoss 46054	. . . . . 6 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
78	77	ffnd 6705	. . . . 5 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
79		fniunfv 7246	. . . . 5 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
80	78, 79	syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
81	72, 80	sseqtrd 3967	. . 3 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
82		ovnovollem2.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
83		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
84		ressxr 11299	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ*
85		xpss2 5675	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
86	84, 85	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ*)
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
88	15, 87	fssd 6722	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ*))
89	83, 88	volicofmpt 46839	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))))
90	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
91		fvexd 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑗)‘𝐴) ∈ V)
92	5, 91, 36	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ((𝐼‘𝑗)‘𝐴))
93	92, 13	eqeltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
94		1st2nd2 8027	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
95	93, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
96	95	fveq2d 6884	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩))
97		df-ov 7418	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
98	97	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
100	48, 96, 99	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
101	32, 50, 100	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
102	101	fveq2d 6884	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))
103		xp1st 8020	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
104	93, 103	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
105		xp2nd 8021	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
106	93, 105	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
107		volicore 47423	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
108	104, 106, 107	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
109	102, 108	eqeltrd 2860	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
110	109	recnd 11283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
111		2fveq3 6885	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
112	111	prodsn 16071	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
113	90, 110, 112	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
114	113, 102	eqtr2d 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
115	114	mpteq2dva 5198	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
116	89, 115	eqtrd 2795	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
117	116	fveq2d 6884	. . . 4 ⊢ (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
118	82, 117	eqtr4d 2798	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
119	81, 118	jca 521	. 2 ⊢ (𝜑 → (𝐵 ⊆ ∪ ran ([,) ∘ 𝐹) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))))
120		coeq2 5839	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ([,) ∘ 𝑓) = ([,) ∘ 𝐹))
121	120	rneqd 5923	. . . . . 6 ⊢ (𝑓 = 𝐹 → ran ([,) ∘ 𝑓) = ran ([,) ∘ 𝐹))
122	121	unieqd 4880	. . . . 5 ⊢ (𝑓 = 𝐹 → ∪ ran ([,) ∘ 𝑓) = ∪ ran ([,) ∘ 𝐹))
123	122	sseq2d 3963	. . . 4 ⊢ (𝑓 = 𝐹 → (𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ↔ 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹)))
124		coeq2 5839	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((vol ∘ [,)) ∘ 𝑓) = ((vol ∘ [,)) ∘ 𝐹))
125	124	fveq2d 6884	. . . . 5 ⊢ (𝑓 = 𝐹 → (Σ^‘((vol ∘ [,)) ∘ 𝑓)) = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
126	125	eqeq2d 2771	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))))
127	123, 126	anbi12d 644	. . 3 ⊢ (𝑓 = 𝐹 → ((𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))) ↔ (𝐵 ⊆ ∪ ran ([,) ∘ 𝐹) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))))
128	127	rspcev 3576	. 2 ⊢ ((𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐵 ⊆ ∪ ran ([,) ∘ 𝐹) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))
129	21, 119, 128	syl2anc 596	1 ⊢ (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ⟨cop 4590  ∪ cuni 4867  ∪ ciun 4951   ↦ cmpt 5186   × cxp 5653  dom cdm 5655  ran crn 5656   ∘ ccom 5659  Fun wfun 6528   Fn wfn 6529  ⟶wf 6530  ‘cfv 6534  (class class class)co 7415  1^st c1st 7986  2^nd c2nd 7987   ↑_m cmap 8830  Xcixp 8908  ℂcc 11144  ℝcr 11145  ℝ^*cxr 11288  ℕcn 12279  [,)cico 13422  ∏cprod 16014  volcvol 25720  Σ^{^}csumge0 47204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7738  ax-inf2 9624  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7372  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7680  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8282  df-wrecs 8313  df-recs 8362  df-rdg 8401  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-fi 9385  df-sup 9416  df-inf 9417  df-oi 9486  df-dju 9928  df-card 9966  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11489  df-neg 11490  df-div 11918  df-nn 12280  df-2 12349  df-3 12350  df-n0 12551  df-z 12638  df-uz 12910  df-q 13020  df-rp 13065  df-xneg 13185  df-xadd 13186  df-xmul 13187  df-ioo 13424  df-ico 13426  df-icc 13427  df-fz 13584  df-fzo 13732  df-fl 13875  df-seq 14088  df-exp 14148  df-hash 14417  df-cj 15208  df-re 15209  df-im 15210  df-sqrt 15344  df-abs 15345  df-clim 15597  df-rlim 15598  df-sum 15796  df-prod 16015  df-rest 17529  df-topgen 17550  df-psmet 21606  df-xmet 21607  df-met 21608  df-bl 21609  df-mopn 21610  df-top 23148  df-topon 23165  df-bases 23200  df-cmp 23641  df-ovol 25721  df-vol 25722

This theorem is used by:  ovnovollem3  47500