Theorem ovnovollem1 47471

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 2763	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩})
2		ovnovollem1.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
4		ovnovollem1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ))
5		elmapi 8851	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
6	4, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
7	6	ffvelcdmda 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
8		fsng 7134	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
9	3, 7, 8	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
10	1, 9	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)})
11	7	snssd 4750	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ × ℝ))
12	10, 11	fssd 6724	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13		reex 11218	. . . . . . . 8 ⊢ ℝ ∈ V
14	13, 13	xpex 7755	. . . . . . 7 ⊢ (ℝ × ℝ) ∈ V
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16		snex 5408	. . . . . . 7 ⊢ {𝐴} ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V)
18	15, 17	elmapd 8842	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}) ↔ {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
19	12, 18	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}))
20		ovnovollem1.i	. . . 4 ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹‘𝑗)⟩})
21	19, 20	fmptd 7110	. . 3 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
22		ovexd 7451	. . . 4 ⊢ (𝜑 → ((ℝ × ℝ) ↑m {𝐴}) ∈ V)
23		nnex 12266	. . . . 5 ⊢ ℕ ∈ V
24	23	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
25	22, 24	elmapd 8842	. . 3 ⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴})))
26	21, 25	mpbird 260	. 2 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
27		ovnovollem1.s	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
28		icof 46036	. . . . . . . . . . 11 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
30		rexpssxrxp 11281	. . . . . . . . . . 11 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
32	29, 31, 6	fcoss 46027	. . . . . . . . 9 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
33	32	ffnd 6707	. . . . . . . 8 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
34		fniunfv 7247	. . . . . . . 8 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
35	33, 34	syl 18	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
36	35	eqcomd 2768	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
37	27, 36	sseqtrd 3970	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
38		ovnovollem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
39		fvex 6895	. . . . . . . 8 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
40	23, 39	iunex 7968	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
42	16	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
43	2	snn0d 4739	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
44	38, 41, 42, 43	mapss2 46023	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})))
45	37, 44	mpbid 235	. . . 4 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
46		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑗𝜑
47		fvexd 6897	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V)
48	46, 24, 47, 2	iunmapsn 46034	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
49	48	eqcomd 2768	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
50		elmapfun 8870	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → Fun 𝐹)
51	4, 50	syl 18	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
52	51	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
53		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
54	6	fdmd 6717	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = ℕ)
55	54	eqcomd 2768	. . . . . . . . . 10 ⊢ (𝜑 → ℕ = dom 𝐹)
56	55	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
57	53, 56	eleqtrd 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
58		fvco 6980	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
59	52, 57, 58	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
60	59	iuneq2dv 4979	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)))
61	60	oveq1d 7431	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
62	10	ffund 6711	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹‘𝑗)⟩})
63		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
64		snex 5408	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V
65	64	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V)
66	20	fvmpt2 7002	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
67	63, 65, 66	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
68	67	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
69	68	funeqd 6559	. . . . . . . . . . . 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 6717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
75	73, 74	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
76	75	eleq2d 2848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
77	76	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
78	72, 77	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗))
79		fvco 6980	. . . . . . . . . 10 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
80	71, 78, 79	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
81	67	fveq1d 6884	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
82	81	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
83		elsni 4604	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
84	83	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
85	84	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
86		fvexd 6897	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑗) ∈ V)
87		fvsng 7181	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
88	2, 86, 87	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
89	88	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
90	82, 85, 89	3eqtrd 2801	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗))
91	90	fveq2d 6886	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗)))
92		eqidd 2763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗)))
93	80, 91, 92	3eqtrd 2801	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗)))
94	93	ixpeq2dva 8922	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)))
95		fvex 6895	. . . . . . . . 9 ⊢ ([,)‘(𝐹‘𝑗)) ∈ V
96	16, 95	ixpconst 8917	. . . . . . . 8 ⊢ X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})
97	96	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
98	94, 97	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
99	98	iuneq2dv 4979	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
100	49, 61, 99	3eqtr4d 2807	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
101	45, 100	sseqtrd 3970	. . 3 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
102		ovnovollem1.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
103		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
104		ressxr 11280	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ*
105		xpss2 5679	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ*)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
108	6, 107	fssd 6724	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ*))
109	103, 108	volicofmpt 46812	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))))
110	67	coeq2d 5846	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ([,) ∘ (𝐼‘𝑗)) = ([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩}))
111	110	fveq1d 6884	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
112	111	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
113		snidg 4624	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
114	2, 113	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
115		dmsnopg 6213	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ V → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
116	86, 115	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
117	114, 116	eleqtrrd 2865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
118	117	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
119		fvco 6980	. . . . . . . . . . . . . 14 ⊢ ((Fun {⟨𝐴, (𝐹‘𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
120	62, 118, 119	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
121		fvexd 6897	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V)
122	3, 121, 87	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
123		1st2nd2 8028	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
124	7, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
125	122, 124	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
126	125	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩))
127		df-ov 7419	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
128	127	eqcomi 2771	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
130	126, 129	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
131	112, 120, 130	3eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
132	131	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))
133		xp1st 8021	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
134	7, 133	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
135		xp2nd 8022	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
136	7, 135	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
137		volicore 47396	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
138	134, 136, 137	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
139	132, 138	eqeltrd 2862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
140	139	recnd 11264	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
141		2fveq3 6887	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
142	141	prodsn 16053	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
143	3, 140, 142	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
144	143, 132	eqtr2d 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
145	144	mpteq2dva 5202	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
146	109, 145	eqtrd 2797	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
147	146	fveq2d 6886	. . . 4 ⊢ (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
148	102, 147	eqtrd 2797	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
149	101, 148	jca 521	. 2 ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
150		fveq1 6881	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗))
151	150	coeq2d 5846	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
152	151	fveq1d 6884	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
153	152	ixpeq2dv 8923	. . . . . 6 ⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
154	153	iuneq2d 4985	. . . . 5 ⊢ (𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
155	154	sseq2d 3966	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)))
156		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
157	156	fveq1d 6884	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗))
158	157	coeq2d 5846	. . . . . . . . . 10 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
159	158	fveq1d 6884	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
160	159	fveq2d 6886	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
161	160	prodeq2dv 16013	. . . . . . 7 ⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
162	161	mpteq2dv 5203	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
163	162	fveq2d 6886	. . . . 5 ⊢ (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
164	163	eqeq2d 2773	. . . 4 ⊢ (𝑖 = 𝐼 → (𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
165	155, 164	anbi12d 644	. . 3 ⊢ (𝑖 = 𝐼 → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))))
166	165	rspcev 3579	. 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 2145  ∃wrex 3088  Vcvv 3453   ⊆ wss 3902  𝒫 cpw 4560  {csn 4587  ⟨cop 4593  ∪ cuni 4870  ∪ ciun 4954   ↦ cmpt 5190   × cxp 5657  dom cdm 5659  ran crn 5660   ∘ ccom 5663  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  1^st c1st 7987  2^nd c2nd 7988   ↑_m cmap 8829  Xcixp 8907  ℂcc 11125  ℝcr 11126  ℝ^*cxr 11269  ℕcn 12260  [,)cico 13402  ∏cprod 15994  volcvol 25692  Σ^{^}csumge0 47177

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7681  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-er 8699  df-map 8831  df-pm 8832  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fi 9384  df-sup 9415  df-inf 9416  df-oi 9485  df-dju 9909  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-n0 12532  df-z 12619  df-uz 12891  df-q 13001  df-rp 13045  df-xneg 13165  df-xadd 13166  df-xmul 13167  df-ioo 13404  df-ico 13406  df-icc 13407  df-fz 13564  df-fzo 13712  df-fl 13855  df-seq 14068  df-exp 14128  df-hash 14397  df-cj 15188  df-re 15189  df-im 15190  df-sqrt 15324  df-abs 15325  df-clim 15577  df-rlim 15578  df-sum 15776  df-prod 15995  df-rest 17511  df-topgen 17532  df-psmet 21578  df-xmet 21579  df-met 21580  df-bl 21581  df-mopn 21582  df-top 23120  df-topon 23137  df-bases 23172  df-cmp 23613  df-ovol 25693  df-vol 25694

This theorem is used by:  ovnovollem3  47473