Theorem ovnovollem1 47869

Description: if 𝐹 is a cover of 𝐵 in ℝ, then 𝐼 is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

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

Assertion

Ref	Expression
ovnovollem1	⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))

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

Allowed substitution hints:   𝜑(𝑖)   𝐵(𝑗, 𝑘)   𝐹(𝑖)   𝑉(𝑖, 𝑗)   𝑊(𝑖, 𝑗, 𝑘)   𝑍(𝑗, 𝑘)

Proof of Theorem ovnovollem1

Step	Hyp	Ref	Expression
1		eqidd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩})
2		ovnovollem1.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
4		ovnovollem1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ))
5		elmapi 8894	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
6	4, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
7	6	ffvelcdmda 7105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
8		fsng 7159	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
9	3, 7, 8	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
10	1, 9	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)})
11	7	snssd 4747	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ × ℝ))
12	10, 11	fssd 6746	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13		reex 11315	. . . . . . . 8 ⊢ ℝ ∈ V
14	13, 13	xpex 7788	. . . . . . 7 ⊢ (ℝ × ℝ) ∈ V
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16		snex 5401	. . . . . . 7 ⊢ {𝐴} ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V)
18	15, 17	elmapd 8885	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}) ↔ {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
19	12, 18	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}))
20		ovnovollem1.i	. . . 4 ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹‘𝑗)⟩})
21	19, 20	fmptd 7135	. . 3 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
22		ovexd 7475	. . . 4 ⊢ (𝜑 → ((ℝ × ℝ) ↑m {𝐴}) ∈ V)
23		nnex 12365	. . . . 5 ⊢ ℕ ∈ V
24	23	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
25	22, 24	elmapd 8885	. . 3 ⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴})))
26	21, 25	mpbird 260	. 2 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
27		ovnovollem1.s	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
28		icof 46435	. . . . . . . . . . 11 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
30		rexpssxrxp 11378	. . . . . . . . . . 11 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
32	29, 31, 6	fcoss 46426	. . . . . . . . 9 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
33	32	ffnd 6729	. . . . . . . 8 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
34		fniunfv 7271	. . . . . . . 8 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
35	33, 34	syl 18	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
36	35	eqcomd 2769	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
37	27, 36	sseqtrd 3949	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
38		ovnovollem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
39		fvex 6918	. . . . . . . 8 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
40	23, 39	iunex 8001	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
42	16	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
43	2	snn0d 4736	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
44	38, 41, 42, 43	mapss2 46422	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})))
45	37, 44	mpbid 235	. . . 4 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
46		nfv 1949	. . . . . . 7 ⊢ Ⅎ𝑗𝜑
47		fvexd 6920	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V)
48	46, 24, 47, 2	iunmapsn 46433	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
49	48	eqcomd 2769	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
50		elmapfun 8913	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → Fun 𝐹)
51	4, 50	syl 18	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
52	51	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
53		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
54	6	fdmd 6739	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = ℕ)
55	54	eqcomd 2769	. . . . . . . . . 10 ⊢ (𝜑 → ℕ = dom 𝐹)
56	55	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
57	53, 56	eleqtrd 2866	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
58		fvco 7003	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
59	52, 57, 58	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
60	59	iuneq2dv 4979	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)))
61	60	oveq1d 7455	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
62	10	ffund 6733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹‘𝑗)⟩})
63		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
64		snex 5401	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V
65	64	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V)
66	20	fvmpt2 7025	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
67	63, 65, 66	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
68	67	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
69	68	funeqd 6578	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {⟨𝐴, (𝐹‘𝑗)⟩}))
70	62, 69	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗))
71	70	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗))
72		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴})
73	68	dmeqd 5893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {⟨𝐴, (𝐹‘𝑗)⟩})
74	10	fdmd 6739	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
75	73, 74	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
76	75	eleq2d 2850	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
77	76	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
78	72, 77	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗))
79		fvco 7003	. . . . . . . . . 10 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
80	71, 78, 79	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
81	67	fveq1d 6907	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
82	81	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
83		elsni 4601	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
84	83	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
85	84	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
86		fvexd 6920	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑗) ∈ V)
87		fvsng 7205	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
88	2, 86, 87	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
89	88	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
90	82, 85, 89	3eqtrd 2802	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗))
91	90	fveq2d 6909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗)))
92		eqidd 2764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗)))
93	80, 91, 92	3eqtrd 2802	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗)))
94	93	ixpeq2dva 8965	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)))
95		fvex 6918	. . . . . . . . 9 ⊢ ([,)‘(𝐹‘𝑗)) ∈ V
96	16, 95	ixpconst 8960	. . . . . . . 8 ⊢ X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})
97	96	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
98	94, 97	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
99	98	iuneq2dv 4979	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
100	49, 61, 99	3eqtr4d 2808	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
101	45, 100	sseqtrd 3949	. . 3 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
102		ovnovollem1.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
103		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
104		ressxr 11377	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ*
105		xpss2 5675	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ*)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
108	6, 107	fssd 6746	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ*))
109	103, 108	volicofmpt 47210	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))))
110	67	coeq2d 5845	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ([,) ∘ (𝐼‘𝑗)) = ([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩}))
111	110	fveq1d 6907	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
112	111	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
113		snidg 4621	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
114	2, 113	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
115		dmsnopg 6226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ V → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
116	86, 115	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
117	114, 116	eleqtrrd 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
118	117	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
119		fvco 7003	. . . . . . . . . . . . . 14 ⊢ ((Fun {⟨𝐴, (𝐹‘𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
120	62, 118, 119	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
121		fvexd 6920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V)
122	3, 121, 87	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
123		1st2nd2 8061	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
124	7, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
125	122, 124	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
126	125	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩))
127		df-ov 7443	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
128	127	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
130	126, 129	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
131	112, 120, 130	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
132	131	fveq2d 6909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))
133		xp1st 8054	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
134	7, 133	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
135		xp2nd 8055	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
136	7, 135	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
137		volicore 47794	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
138	134, 136, 137	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
139	132, 138	eqeltrd 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
140	139	recnd 11361	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
141		2fveq3 6910	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
142	141	prodsn 16155	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
143	3, 140, 142	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
144	143, 132	eqtr2d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
145	144	mpteq2dva 5201	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
146	109, 145	eqtrd 2798	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
147	146	fveq2d 6909	. . . 4 ⊢ (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
148	102, 147	eqtrd 2798	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
149	101, 148	jca 521	. 2 ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
150		fveq1 6904	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗))
151	150	coeq2d 5845	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
152	151	fveq1d 6907	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
153	152	ixpeq2dv 8966	. . . . . 6 ⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
154	153	iuneq2d 4984	. . . . 5 ⊢ (𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
155	154	sseq2d 3945	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)))
156		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
157	156	fveq1d 6907	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗))
158	157	coeq2d 5845	. . . . . . . . . 10 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
159	158	fveq1d 6907	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
160	159	fveq2d 6909	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
161	160	prodeq2dv 16116	. . . . . . 7 ⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
162	161	mpteq2dv 5202	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
163	162	fveq2d 6909	. . . . 5 ⊢ (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
164	163	eqeq2d 2774	. . . 4 ⊢ (𝑖 = 𝐼 → (𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
165	155, 164	anbi12d 644	. . 3 ⊢ (𝑖 = 𝐼 → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))))
166	165	rspcev 3580	. 2 ⊢ ((𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))
167	26, 149, 166	syl2anc 596	1 ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900  𝒫 cpw 4560  {csn 4588  ⟨cop 4838  ∪ cuni 4870  ∪ ciun 4954   ↦ cmpt 5189   × cxp 5653  dom cdm 5655  ran crn 5656   ∘ ccom 5659  Fun wfun 6549   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440  1^st c1st 8020  2^nd c2nd 8021   ↑_m cmap 8872  Xcixp 8950  ℂcc 11222  ℝcr 11223  ℝ^*cxr 11366  ℕcn 12359  [,)cico 13502  ∏cprod 16098  volcvol 25811  Σ^{^}csumge0 47575

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-inf2 9666  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301  ax-pre-sup 11302

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  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 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-map 8874  df-pm 8875  df-ixp 8951  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fi 9427  df-sup 9458  df-inf 9459  df-oi 9528  df-dju 10006  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998  df-nn 12360  df-2 12429  df-3 12430  df-n0 12631  df-z 12718  df-uz 12990  df-q 13100  df-rp 13145  df-xneg 13265  df-xadd 13266  df-xmul 13267  df-ioo 13504  df-ico 13506  df-icc 13507  df-fz 13664  df-fzo 13813  df-fl 13956  df-seq 14169  df-exp 14229  df-hash 14499  df-cj 15292  df-re 15293  df-im 15294  df-sqrt 15428  df-abs 15429  df-clim 15681  df-rlim 15682  df-sum 15880  df-prod 16099  df-rest 17619  df-topgen 17640  df-psmet 21697  df-xmet 21698  df-met 21699  df-bl 21700  df-mopn 21701  df-top 23239  df-topon 23256  df-bases 23291  df-cmp 23732  df-ovol 25812  df-vol 25813

This theorem is used by:  ovnovollem3  47871