Theorem ovnovollem1 46685

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 2736	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩})
2		ovnovollem1.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
4		ovnovollem1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ))
5		elmapi 8863	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
7	6	ffvelcdmda 7074	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
8		fsng 7127	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
9	3, 7, 8	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
10	1, 9	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)})
11	7	snssd 4785	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ × ℝ))
12	10, 11	fssd 6723	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13		reex 11220	. . . . . . . 8 ⊢ ℝ ∈ V
14	13, 13	xpex 7747	. . . . . . 7 ⊢ (ℝ × ℝ) ∈ V
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16		snex 5406	. . . . . . 7 ⊢ {𝐴} ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V)
18	15, 17	elmapd 8854	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}) ↔ {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
19	12, 18	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑m {𝐴}))
20		ovnovollem1.i	. . . 4 ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹‘𝑗)⟩})
21	19, 20	fmptd 7104	. . 3 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴}))
22		ovexd 7440	. . . 4 ⊢ (𝜑 → ((ℝ × ℝ) ↑m {𝐴}) ∈ V)
23		nnex 12246	. . . . 5 ⊢ ℕ ∈ V
24	23	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
25	22, 24	elmapd 8854	. . 3 ⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑m {𝐴})))
26	21, 25	mpbird 257	. 2 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ))
27		ovnovollem1.s	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
28		icof 45243	. . . . . . . . . . 11 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
30		rexpssxrxp 11280	. . . . . . . . . . 11 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
32	29, 31, 6	fcoss 45234	. . . . . . . . 9 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
33	32	ffnd 6707	. . . . . . . 8 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
34		fniunfv 7239	. . . . . . . 8 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
35	33, 34	syl 17	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
36	35	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
37	27, 36	sseqtrd 3995	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
38		ovnovollem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
39		fvex 6889	. . . . . . . 8 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
40	23, 39	iunex 7967	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
42	16	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
43	2	snn0d 4751	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
44	38, 41, 42, 43	mapss2 45229	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})))
45	37, 44	mpbid 232	. . . 4 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))
46		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑗𝜑
47		fvexd 6891	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V)
48	46, 24, 47, 2	iunmapsn 45241	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
49	48	eqcomd 2741	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
50		elmapfun 8880	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑m ℕ) → Fun 𝐹)
51	4, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
53		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
54	6	fdmd 6716	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = ℕ)
55	54	eqcomd 2741	. . . . . . . . . 10 ⊢ (𝜑 → ℕ = dom 𝐹)
56	55	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
57	53, 56	eleqtrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
58		fvco 6977	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
59	52, 57, 58	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
60	59	iuneq2dv 4992	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)))
61	60	oveq1d 7420	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
62	10	ffund 6710	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹‘𝑗)⟩})
63		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
64		snex 5406	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V
65	64	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V)
66	20	fvmpt2 6997	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
67	63, 65, 66	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
68	67	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
69	68	funeqd 6558	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {⟨𝐴, (𝐹‘𝑗)⟩}))
70	62, 69	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗))
71	70	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗))
72		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴})
73	68	dmeqd 5885	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {⟨𝐴, (𝐹‘𝑗)⟩})
74	10	fdmd 6716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
75	73, 74	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
76	75	eleq2d 2820	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
77	76	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
78	72, 77	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗))
79		fvco 6977	. . . . . . . . . 10 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
80	71, 78, 79	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
81	67	fveq1d 6878	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
82	81	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
83		elsni 4618	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
84	83	fveq2d 6880	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
85	84	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
86		fvexd 6891	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑗) ∈ V)
87		fvsng 7172	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
88	2, 86, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
89	88	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
90	82, 85, 89	3eqtrd 2774	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗))
91	90	fveq2d 6880	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗)))
92		eqidd 2736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗)))
93	80, 91, 92	3eqtrd 2774	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗)))
94	93	ixpeq2dva 8926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)))
95		fvex 6889	. . . . . . . . 9 ⊢ ([,)‘(𝐹‘𝑗)) ∈ V
96	16, 95	ixpconst 8921	. . . . . . . 8 ⊢ X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})
97	96	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
98	94, 97	eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
99	98	iuneq2dv 4992	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}))
100	49, 61, 99	3eqtr4d 2780	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
101	45, 100	sseqtrd 3995	. . 3 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
102		ovnovollem1.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
103		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
104		ressxr 11279	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ*
105		xpss2 5674	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ*)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
108	6, 107	fssd 6723	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ*))
109	103, 108	volicofmpt 46026	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))))
110	67	coeq2d 5842	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ([,) ∘ (𝐼‘𝑗)) = ([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩}))
111	110	fveq1d 6878	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
112	111	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
113		snidg 4636	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
114	2, 113	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
115		dmsnopg 6202	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ V → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
116	86, 115	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
117	114, 116	eleqtrrd 2837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
118	117	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
119		fvco 6977	. . . . . . . . . . . . . 14 ⊢ ((Fun {⟨𝐴, (𝐹‘𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
120	62, 118, 119	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
121		fvexd 6891	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V)
122	3, 121, 87	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
123		1st2nd2 8027	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
124	7, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
125	122, 124	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = ⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
126	125	fveq2d 6880	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩))
127		df-ov 7408	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩)
128	127	eqcomi 2744	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))⟩) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
130	126, 129	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
131	112, 120, 130	3eqtrd 2774	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))
132	131	fveq2d 6880	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))
133		xp1st 8020	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
134	7, 133	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st ‘(𝐹‘𝑗)) ∈ ℝ)
135		xp2nd 8021	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
136	7, 135	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd ‘(𝐹‘𝑗)) ∈ ℝ)
137		volicore 46610	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
138	134, 136, 137	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ)
139	132, 138	eqeltrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
140	139	recnd 11263	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
141		2fveq3 6881	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
142	141	prodsn 15978	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
143	3, 140, 142	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
144	143, 132	eqtr2d 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
145	144	mpteq2dva 5214	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
146	109, 145	eqtrd 2770	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
147	146	fveq2d 6880	. . . 4 ⊢ (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
148	102, 147	eqtrd 2770	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
149	101, 148	jca 511	. 2 ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
150		fveq1 6875	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗))
151	150	coeq2d 5842	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
152	151	fveq1d 6878	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
153	152	ixpeq2dv 8927	. . . . . 6 ⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
154	153	iuneq2d 4998	. . . . 5 ⊢ (𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
155	154	sseq2d 3991	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)))
156		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
157	156	fveq1d 6878	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗))
158	157	coeq2d 5842	. . . . . . . . . 10 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
159	158	fveq1d 6878	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
160	159	fveq2d 6880	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
161	160	prodeq2dv 15938	. . . . . . 7 ⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
162	161	mpteq2dv 5215	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
163	162	fveq2d 6880	. . . . 5 ⊢ (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
164	163	eqeq2d 2746	. . . 4 ⊢ (𝑖 = 𝐼 → (𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
165	155, 164	anbi12d 632	. . 3 ⊢ (𝑖 = 𝐼 → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))))
166	165	rspcev 3601	. 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 2108  ∃wrex 3060  Vcvv 3459   ⊆ wss 3926  𝒫 cpw 4575  {csn 4601  ⟨cop 4607  ∪ cuni 4883  ∪ ciun 4967   ↦ cmpt 5201   × cxp 5652  dom cdm 5654  ran crn 5655   ∘ ccom 5658  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405  1^st c1st 7986  2^nd c2nd 7987   ↑_m cmap 8840  Xcixp 8911  ℂcc 11127  ℝcr 11128  ℝ^*cxr 11268  ℕcn 12240  [,)cico 13364  ∏cprod 15919  volcvol 25416  Σ^{^}csumge0 46391

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-inf2 9655  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-pre-sup 11207

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7671  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8719  df-map 8842  df-pm 8843  df-ixp 8912  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fi 9423  df-sup 9454  df-inf 9455  df-oi 9524  df-dju 9915  df-card 9953  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-n0 12502  df-z 12589  df-uz 12853  df-q 12965  df-rp 13009  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ioo 13366  df-ico 13368  df-icc 13369  df-fz 13525  df-fzo 13672  df-fl 13809  df-seq 14020  df-exp 14080  df-hash 14349  df-cj 15118  df-re 15119  df-im 15120  df-sqrt 15254  df-abs 15255  df-clim 15504  df-rlim 15505  df-sum 15703  df-prod 15920  df-rest 17436  df-topgen 17457  df-psmet 21307  df-xmet 21308  df-met 21309  df-bl 21310  df-mopn 21311  df-top 22832  df-topon 22849  df-bases 22884  df-cmp 23325  df-ovol 25417  df-vol 25418

This theorem is referenced by:  ovnovollem3  46687