ovnovollem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ovnovollem1		Structured version Visualization version GIF version

Theorem ovnovollem1 45359

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 2734	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩})
2		ovnovollem1.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉)
4		ovnovollem1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑_m ℕ))
5		elmapi 8840	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑_m ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
7	6	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ × ℝ))
8		fsng 7132	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
9	3, 7, 8	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {⟨𝐴, (𝐹‘𝑗)⟩} = {⟨𝐴, (𝐹‘𝑗)⟩}))
10	1, 9	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶{(𝐹‘𝑗)})
11	7	snssd 4812	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ × ℝ))
12	10, 11	fssd 6733	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13		reex 11198	. . . . . . . 8 ⊢ ℝ ∈ V
14	13, 13	xpex 7737	. . . . . . 7 ⊢ (ℝ × ℝ) ∈ V
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16		snex 5431	. . . . . . 7 ⊢ {𝐴} ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V)
18	15, 17	elmapd 8831	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑_m {𝐴}) ↔ {⟨𝐴, (𝐹‘𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
19	12, 18	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ ((ℝ × ℝ) ↑_m {𝐴}))
20		ovnovollem1.i	. . . 4 ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹‘𝑗)⟩})
21	19, 20	fmptd 7111	. . 3 ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑_m {𝐴}))
22		ovexd 7441	. . . 4 ⊢ (𝜑 → ((ℝ × ℝ) ↑_m {𝐴}) ∈ V)
23		nnex 12215	. . . . 5 ⊢ ℕ ∈ V
24	23	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
25	22, 24	elmapd 8831	. . 3 ⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑_m {𝐴}) ↑_m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑_m {𝐴})))
26	21, 25	mpbird 257	. 2 ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑_m {𝐴}) ↑_m ℕ))
27		ovnovollem1.s	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹))
28		icof 43904	. . . . . . . . . . 11 ⊢ [,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → [,):(ℝ^* × ℝ^)⟶𝒫 ℝ^)
30		rexpssxrxp 11256	. . . . . . . . . . 11 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*))
32	29, 31, 6	fcoss 43895	. . . . . . . . 9 ⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ^*)
33	32	ffnd 6716	. . . . . . . 8 ⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
34		fniunfv 7243	. . . . . . . 8 ⊢ (([,) ∘ 𝐹) Fn ℕ → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
35	33, 34	syl 17	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,) ∘ 𝐹))
36	35	eqcomd 2739	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
37	27, 36	sseqtrd 4022	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
38		ovnovollem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
39		fvex 6902	. . . . . . . 8 ⊢ (([,) ∘ 𝐹)‘𝑗) ∈ V
40	23, 39	iunex 7952	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
42	16	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝐴} ∈ V)
43	2	snn0d 4779	. . . . . 6 ⊢ (𝜑 → {𝐴} ≠ ∅)
44	38, 41, 42, 43	mapss2 43890	. . . . 5 ⊢ (𝜑 → (𝐵 ⊆ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵 ↑_m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑_m {𝐴})))
45	37, 44	mpbid 231	. . . 4 ⊢ (𝜑 → (𝐵 ↑_m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑_m {𝐴}))
46		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑗𝜑
47		fvexd 6904	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V)
48	46, 24, 47, 2	iunmapsn 43902	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑_m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
49	48	eqcomd 2739	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑_m {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
50		elmapfun 8857	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((ℝ × ℝ) ↑_m ℕ) → Fun 𝐹)
51	4, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
52	51	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹)
53		simpr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
54	6	fdmd 6726	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = ℕ)
55	54	eqcomd 2739	. . . . . . . . . 10 ⊢ (𝜑 → ℕ = dom 𝐹)
56	55	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹)
57	53, 56	eleqtrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
58		fvco 6987	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
59	52, 57, 58	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗)))
60	59	iuneq2dv 5021	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)))
61	60	oveq1d 7421	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑_m {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
62	10	ffund 6719	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹‘𝑗)⟩})
63		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
64		snex 5431	. . . . . . . . . . . . . . . 16 ⊢ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V
65	64	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V)
66	20	fvmpt2 7007	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹‘𝑗)⟩} ∈ V) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
67	63, 65, 66	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
68	67	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {⟨𝐴, (𝐹‘𝑗)⟩})
69	68	funeqd 6568	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {⟨𝐴, (𝐹‘𝑗)⟩}))
70	62, 69	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗))
71	70	adantr 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗))
72		simpr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴})
73	68	dmeqd 5904	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {⟨𝐴, (𝐹‘𝑗)⟩})
74	10	fdmd 6726	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
75	73, 74	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴})
76	75	eleq2d 2820	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
77	76	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴}))
78	72, 77	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗))
79		fvco 6987	. . . . . . . . . 10 ⊢ ((Fun (𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
80	71, 78, 79	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘)))
81	67	fveq1d 6891	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
82	81	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘))
83		elsni 4645	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
84	83	fveq2d 6893	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
85	84	adantl 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴))
86		fvexd 6904	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑗) ∈ V)
87		fvsng 7175	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
88	2, 86, 87	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
89	88	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
90	82, 85, 89	3eqtrd 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗))
91	90	fveq2d 6893	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗)))
92		eqidd 2734	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗)))
93	80, 91, 92	3eqtrd 2777	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗)))
94	93	ixpeq2dva 8903	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)))
95		fvex 6902	. . . . . . . . 9 ⊢ ([,)‘(𝐹‘𝑗)) ∈ V
96	16, 95	ixpconst 8898	. . . . . . . 8 ⊢ X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑_m {𝐴})
97	96	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
98	94, 97	eqtrd 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
99	98	iuneq2dv 5021	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑_m {𝐴}))
100	49, 61, 99	3eqtr4d 2783	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑_m {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
101	45, 100	sseqtrd 4022	. . 3 ⊢ (𝜑 → (𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
102		ovnovollem1.z	. . . 4 ⊢ (𝜑 → 𝑍 = (Σ^{^}‘((vol ∘ [,)) ∘ 𝐹)))
103		nfcv 2904	. . . . . . 7 ⊢ Ⅎ𝑗𝐹
104		ressxr 11255	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ^*
105		xpss2 5696	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ^* → (ℝ × ℝ) ⊆ (ℝ × ℝ^*))
106	104, 105	ax-mp 5	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ × ℝ^*)
107	106	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ^*))
108	6, 107	fssd 6733	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ^*))
109	103, 108	volicofmpt 44700	. . . . . 6 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))))))
110	67	coeq2d 5861	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ([,) ∘ (𝐼‘𝑗)) = ([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩}))
111	110	fveq1d 6891	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
112	111	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴))
113		snidg 4662	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
114	2, 113	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
115		dmsnopg 6210	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ V → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
116	86, 115	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom {⟨𝐴, (𝐹‘𝑗)⟩} = {𝐴})
117	114, 116	eleqtrrd 2837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
118	117	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩})
119		fvco 6987	. . . . . . . . . . . . . 14 ⊢ ((Fun {⟨𝐴, (𝐹‘𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹‘𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
120	62, 118, 119	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹‘𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)))
121		fvexd 6904	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V)
122	3, 121, 87	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = (𝐹‘𝑗))
123		1st2nd2 8011	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (𝐹‘𝑗) = ⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩)
124	7, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = ⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩)
125	122, 124	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴) = ⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩)
126	125	fveq2d 6893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ([,)‘⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩))
127		df-ov 7409	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))) = ([,)‘⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩)
128	127	eqcomi 2742	. . . . . . . . . . . . . . 15 ⊢ ([,)‘⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩) = ((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗)))
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘⟨(1^st ‘(𝐹‘𝑗)), (2^nd ‘(𝐹‘𝑗))⟩) = ((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))))
130	126, 129	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹‘𝑗)⟩}‘𝐴)) = ((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))))
131	112, 120, 130	3eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))))
132	131	fveq2d 6893	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗)))))
133		xp1st 8004	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘𝑗)) ∈ ℝ)
134	7, 133	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1^st ‘(𝐹‘𝑗)) ∈ ℝ)
135		xp2nd 8005	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) → (2^nd ‘(𝐹‘𝑗)) ∈ ℝ)
136	7, 135	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2^nd ‘(𝐹‘𝑗)) ∈ ℝ)
137		volicore 45284	. . . . . . . . . . . 12 ⊢ (((1^st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑗)) ∈ ℝ) → (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗)))) ∈ ℝ)
138	134, 136, 137	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗)))) ∈ ℝ)
139	132, 138	eqeltrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ)
140	139	recnd 11239	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ)
141		2fveq3 6894	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
142	141	prodsn 15903	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
143	3, 140, 142	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)))
144	143, 132	eqtr2d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
145	144	mpteq2dva 5248	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1^st ‘(𝐹‘𝑗))[,)(2^nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
146	109, 145	eqtrd 2773	. . . . 5 ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
147	146	fveq2d 6893	. . . 4 ⊢ (𝜑 → (Σ^{^}‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
148	102, 147	eqtrd 2773	. . 3 ⊢ (𝜑 → 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
149	101, 148	jca 513	. 2 ⊢ (𝜑 → ((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
150		fveq1 6888	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗))
151	150	coeq2d 5861	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
152	151	fveq1d 6891	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
153	152	ixpeq2dv 8904	. . . . . 6 ⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
154	153	iuneq2d 5026	. . . . 5 ⊢ (𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))
155	154	sseq2d 4014	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)))
156		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
157	156	fveq1d 6891	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗))
158	157	coeq2d 5861	. . . . . . . . . 10 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗)))
159	158	fveq1d 6891	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘))
160	159	fveq2d 6893	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
161	160	prodeq2dv 15864	. . . . . . 7 ⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))
162	161	mpteq2dv 5250	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))
163	162	fveq2d 6893	. . . . 5 ⊢ (𝑖 = 𝐼 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))
164	163	eqeq2d 2744	. . . 4 ⊢ (𝑖 = 𝐼 → (𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))
165	155, 164	anbi12d 632	. . 3 ⊢ (𝑖 = 𝐼 → (((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))))
166	165	rspcev 3613	. 2 ⊢ ((𝐼 ∈ (((ℝ × ℝ) ↑_m {𝐴}) ↑_m ℕ) ∧ ((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ) ↑_m {𝐴}) ↑_m ℕ)((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))
167	26, 149, 166	syl2anc 585	1 ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑_m {𝐴}) ↑_m ℕ)((𝐵 ↑_m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 Vcvv 3475 ⊆ wss 3948 𝒫 cpw 4602 {csn 4628 ⟨cop 4634 ∪ cuni 4908 ∪ ciun 4997 ↦ cmpt 5231 × cxp 5674 dom cdm 5676 ran crn 5677 ∘ ccom 5680 Fun wfun 6535 Fn wfn 6536 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 1^st c1st 7970 2^nd c2nd 7971 ↑_m cmap 8817 Xcixp 8888 ℂcc 11105 ℝcr 11106 ℝ^*cxr 11244 ℕcn 12209 [,)cico 13323 ∏cprod 15846 volcvol 24972 Σ^{^}csumge0 45065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-dju 9893 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-n0 12470 df-z 12556 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-seq 13964 df-exp 14025 df-hash 14288 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-clim 15429 df-rlim 15430 df-sum 15630 df-prod 15847 df-rest 17365 df-topgen 17386 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-top 22388 df-topon 22405 df-bases 22441 df-cmp 22883 df-ovol 24973 df-vol 24974

This theorem is referenced by: ovnovollem3 45361

W3C validator