Theorem ovnovollem1 46661

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 2731	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩})
2		ovnovollem1.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
4		ovnovollem1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ))
5		elmapi 8825	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
7	6	ffvelcdmda 7059	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
8		fsng 7112	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
9	3, 7, 8	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
10	1, 9	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)})
11	7	snssd 4776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ × ℝ))
12	10, 11	fssd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13		reex 11166	. . . . . . . 8 ⊢ ℝ ∈ V
14	13, 13	xpex 7732	. . . . . . 7 ⊢ (ℝ × ℝ) ∈ V
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16		snex 5394	. . . . . . 7 ⊢ {𝐴} ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V)
18	15, 17	elmapd 8816	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}) ↔ {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
19	12, 18	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}))
20		ovnovollem1.i	. . . 4 ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹‘𝑗)⟩})
21	19, 20	fmptd 7089	. . 3 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
22		ovexd 7425	. . . 4 ⊢ (𝜑 → ((ℝ × ℝ) ↑m {𝐴}) ∈ V)
23		nnex 12199	. . . . 5 ⊢ ℕ ∈ V
24	23	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
25	22, 24	elmapd 8816	. . 3 ⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴})))
26	21, 25	mpbird 257	. 2 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
27		ovnovollem1.s	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
28		icof 45220	. . . . . . . . . . 11 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
30		rexpssxrxp 11226	. . . . . . . . . . 11 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
32	29, 31, 6	fcoss 45211	. . . . . . . . 9 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
33	32	ffnd 6692	. . . . . . . 8 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
34		fniunfv 7224	. . . . . . . 8 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
35	33, 34	syl 17	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
36	35	eqcomd 2736	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
37	27, 36	sseqtrd 3986	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
38		ovnovollem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
39		fvex 6874	. . . . . . . 8 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
40	23, 39	iunex 7950	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
42	16	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
43	2	snn0d 4742	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
44	38, 41, 42, 43	mapss2 45206	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})))
45	37, 44	mpbid 232	. . . 4 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
46		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑗𝜑
47		fvexd 6876	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V)
48	46, 24, 47, 2	iunmapsn 45218	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
49	48	eqcomd 2736	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
50		elmapfun 8842	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → Fun 𝐹)
51	4, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
53		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
54	6	fdmd 6701	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = ℕ)
55	54	eqcomd 2736	. . . . . . . . . 10 ⊢ (𝜑 → ℕ = dom 𝐹)
56	55	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
57	53, 56	eleqtrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
58		fvco 6962	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
59	52, 57, 58	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
60	59	iuneq2dv 4983	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)))
61	60	oveq1d 7405	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
62	10	ffund 6695	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹‘𝑗)⟩})
63		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
64		snex 5394	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V
65	64	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V)
66	20	fvmpt2 6982	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
67	63, 65, 66	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
68	67	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
69	68	funeqd 6541	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {⟨𝐴, (𝐹‘𝑗)⟩}))
70	62, 69	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗))
71	70	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗))
72		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴})
73	68	dmeqd 5872	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {⟨𝐴, (𝐹‘𝑗)⟩})
74	10	fdmd 6701	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
75	73, 74	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
76	75	eleq2d 2815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
77	76	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
78	72, 77	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗))
79		fvco 6962	. . . . . . . . . 10 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
80	71, 78, 79	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
81	67	fveq1d 6863	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
82	81	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
83		elsni 4609	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
84	83	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
85	84	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
86		fvexd 6876	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑗) ∈ V)
87		fvsng 7157	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
88	2, 86, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
89	88	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
90	82, 85, 89	3eqtrd 2769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗))
91	90	fveq2d 6865	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗)))
92		eqidd 2731	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗)))
93	80, 91, 92	3eqtrd 2769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗)))
94	93	ixpeq2dva 8888	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)))
95		fvex 6874	. . . . . . . . 9 ⊢ ([,)‘(𝐹‘𝑗)) ∈ V
96	16, 95	ixpconst 8883	. . . . . . . 8 ⊢ X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})
97	96	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
98	94, 97	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
99	98	iuneq2dv 4983	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
100	49, 61, 99	3eqtr4d 2775	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
101	45, 100	sseqtrd 3986	. . 3 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
102		ovnovollem1.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
103		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
104		ressxr 11225	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ*
105		xpss2 5661	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ*)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
108	6, 107	fssd 6708	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ*))
109	103, 108	volicofmpt 46002	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))))
110	67	coeq2d 5829	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ([,) ∘ (𝐼‘𝑗)) = ([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩}))
111	110	fveq1d 6863	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
112	111	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
113		snidg 4627	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
114	2, 113	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
115		dmsnopg 6189	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ V → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
116	86, 115	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
117	114, 116	eleqtrrd 2832	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
118	117	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
119		fvco 6962	. . . . . . . . . . . . . 14 ⊢ ((Fun {⟨𝐴, (𝐹‘𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
120	62, 118, 119	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
121		fvexd 6876	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V)
122	3, 121, 87	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
123		1st2nd2 8010	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
124	7, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
125	122, 124	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
126	125	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩))
127		df-ov 7393	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
128	127	eqcomi 2739	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
130	126, 129	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
131	112, 120, 130	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
132	131	fveq2d 6865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))
133		xp1st 8003	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
134	7, 133	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
135		xp2nd 8004	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
136	7, 135	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
137		volicore 46586	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
138	134, 136, 137	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
139	132, 138	eqeltrd 2829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
140	139	recnd 11209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
141		2fveq3 6866	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
142	141	prodsn 15935	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
143	3, 140, 142	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
144	143, 132	eqtr2d 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
145	144	mpteq2dva 5203	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
146	109, 145	eqtrd 2765	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
147	146	fveq2d 6865	. . . 4 ⊢ (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
148	102, 147	eqtrd 2765	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
149	101, 148	jca 511	. 2 ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
150		fveq1 6860	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗))
151	150	coeq2d 5829	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
152	151	fveq1d 6863	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
153	152	ixpeq2dv 8889	. . . . . 6 ⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
154	153	iuneq2d 4989	. . . . 5 ⊢ (𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
155	154	sseq2d 3982	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)))
156		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
157	156	fveq1d 6863	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗))
158	157	coeq2d 5829	. . . . . . . . . 10 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
159	158	fveq1d 6863	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
160	159	fveq2d 6865	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
161	160	prodeq2dv 15895	. . . . . . 7 ⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
162	161	mpteq2dv 5204	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
163	162	fveq2d 6865	. . . . 5 ⊢ (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
164	163	eqeq2d 2741	. . . 4 ⊢ (𝑖 = 𝐼 → (𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
165	155, 164	anbi12d 632	. . 3 ⊢ (𝑖 = 𝐼 → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))))
166	165	rspcev 3591	. 2 ⊢ ((𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))
167	26, 149, 166	syl2anc 584	1 ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  Vcvv 3450   ⊆ wss 3917  𝒫 cpw 4566  {csn 4592  ⟨cop 4598  ∪ cuni 4874  ∪ ciun 4958   ↦ cmpt 5191   × cxp 5639  dom cdm 5641  ran crn 5642   ∘ ccom 5645  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  1^st c1st 7969  2^nd c2nd 7970   ↑_m cmap 8802  Xcixp 8873  ℂcc 11073  ℝcr 11074  ℝ^*cxr 11214  ℕcn 12193  [,)cico 13315  ∏cprod 15876  volcvol 25371  Σ^{^}csumge0 46367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8674  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fi 9369  df-sup 9400  df-inf 9401  df-oi 9470  df-dju 9861  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450  df-z 12537  df-uz 12801  df-q 12915  df-rp 12959  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-ioo 13317  df-ico 13319  df-icc 13320  df-fz 13476  df-fzo 13623  df-fl 13761  df-seq 13974  df-exp 14034  df-hash 14303  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15461  df-rlim 15462  df-sum 15660  df-prod 15877  df-rest 17392  df-topgen 17413  df-psmet 21263  df-xmet 21264  df-met 21265  df-bl 21266  df-mopn 21267  df-top 22788  df-topon 22805  df-bases 22840  df-cmp 23281  df-ovol 25372  df-vol 25373

This theorem is referenced by:  ovnovollem3  46663