hoidmv1le - Mathbox for Glauco Siliprandi

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

Theorem hoidmv1le 41380

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
hoidmv1le.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hoidmv1le.z	⊢ (𝜑 → 𝑍 ∈ 𝑉)
hoidmv1le.x	⊢ 𝑋 = {𝑍}
hoidmv1le.a	⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
hoidmv1le.b	⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
hoidmv1le.c	⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_𝑚 𝑋))
hoidmv1le.d	⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_𝑚 𝑋))
hoidmv1le.s	⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))

**Assertion**
Ref	Expression
hoidmv1le	⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑗,𝑘,𝑥 𝐵,𝑎,𝑏,𝑗,𝑘,𝑥 𝐶,𝑎,𝑏,𝑗,𝑘,𝑥 𝐷,𝑎,𝑏,𝑗,𝑘,𝑥 𝑘,𝑉 𝑋,𝑎,𝑏,𝑘,𝑥 𝑗,𝑍,𝑘,𝑥 𝜑,𝑎,𝑏,𝑗,𝑥 Allowed substitution hints: 𝜑(𝑘) 𝐿(𝑥,𝑗,𝑘,𝑎,𝑏) 𝑉(𝑥,𝑗,𝑎,𝑏) 𝑋(𝑗) 𝑍(𝑎,𝑏)

Proof of Theorem hoidmv1le Dummy variables 𝑖 𝑤 𝑧 𝑦 𝑙 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hoidmv1le.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
2		hoidmv1le.z	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
3		snidg 4364	. . . . . . . . . . . 12 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
4	2, 3	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
5		hoidmv1le.x	. . . . . . . . . . 11 ⊢ 𝑋 = {𝑍}
6	4, 5	syl6eleqr 2855	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑋)
7	1, 6	ffvelrnd 6550	. . . . . . . . 9 ⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ)
8		hoidmv1le.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
9	8, 6	ffvelrnd 6550	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ)
10	7, 9	resubcld 10712	. . . . . . . 8 ⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ)
11	10	rexrd 10343	. . . . . . 7 ⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ^*)
12		pnfxr 10346	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
13	12	a1i 11	. . . . . . 7 ⊢ (𝜑 → +∞ ∈ ℝ^*)
14	10	ltpnfd 12155	. . . . . . 7 ⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) < +∞)
15	11, 13, 14	xrltled 12183	. . . . . 6 ⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
16	15	ad2antrr 717	. . . . 5 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
17		id 22	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
18	17	eqcomd 2771	. . . . . 6 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
19	18	adantl 473	. . . . 5 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
20	16, 19	breqtrd 4835	. . . 4 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
21		simpl 474	. . . . 5 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)))
22		simpr 477	. . . . . 6 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
23		nnex 11281	. . . . . . . 8 ⊢ ℕ ∈ V
24	23	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25		hoidmv1le.l	. . . . . . . . . . . 12 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
26	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 = {𝑍})
27		snfi 8245	. . . . . . . . . . . . . . 15 ⊢ {𝑍} ∈ Fin
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑍} ∈ Fin)
29	26, 28	eqeltrd 2844	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ Fin)
30	29	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
31	6	ne0d 4086	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ≠ ∅)
32	31	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33		hoidmv1le.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_𝑚 𝑋))
34	33	ffvelrnda 6549	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_𝑚 𝑋))
35		elmapi 8082	. . . . . . . . . . . . 13 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_𝑚 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
36	34, 35	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
37		hoidmv1le.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_𝑚 𝑋))
38	37	ffvelrnda 6549	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_𝑚 𝑋))
39		elmapi 8082	. . . . . . . . . . . . 13 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_𝑚 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
40	38, 39	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
41	25, 30, 32, 36, 40	hoidmvn0val 41370	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
42	5	prodeq1i 14933	. . . . . . . . . . . 12 ⊢ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
43	42	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
44	2	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑉)
45	6	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑋)
46	36, 45	ffvelrnd 6550	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
47	40, 45	ffvelrnd 6550	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
48		volicore 41367	. . . . . . . . . . . . . 14 ⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
49	46, 47, 48	syl2anc 579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
50	49	recnd 10322	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ)
51		fveq2 6375	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑍 → ((𝐶‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑍))
52		fveq2 6375	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑍 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑍))
53	51, 52	oveq12d 6860	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑍 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
54	53	fveq2d 6379	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑍 → (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
55	54	prodsn 14977	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ 𝑉 ∧ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
56	44, 50, 55	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
57	41, 43, 56	3eqtrd 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
58	57	mpteq2dva 4903	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
59		fveq2 6375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑙 → (𝑎‘𝑘) = (𝑎‘𝑙))
60		fveq2 6375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑙 → (𝑏‘𝑘) = (𝑏‘𝑙))
61	59, 60	oveq12d 6860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑎‘𝑙)[,)(𝑏‘𝑙)))
62	61	fveq2d 6379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
63	62	cbvprodv 14931	. . . . . . . . . . . . . . . . 17 ⊢ ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))
64		ifeq2 4248	. . . . . . . . . . . . . . . . 17 ⊢ (∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
66	65	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ (ℝ ↑_𝑚 𝑥) ∧ 𝑏 ∈ (ℝ ↑_𝑚 𝑥)) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
67	66	mpt2eq3ia 6918	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
68	67	mpteq2i 4900	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
69	25, 68	eqtri 2787	. . . . . . . . . . . 12 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
70	69, 30, 36, 40	hoidmvcl 41368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
71		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
72	70, 71	fmptd 6574	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
73		icossicc 12463	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
74	73	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
75	72, 74	fssd 6237	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
76	58, 75	feq1dd 39926	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
77	76	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
78	24, 77	sge0repnf 41172	. . . . . 6 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞))
79	22, 78	mpbird 248	. . . . 5 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
80	9	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) ∈ ℝ)
81	7	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐵‘𝑍) ∈ ℝ)
82		simplr 785	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) < (𝐵‘𝑍))
83		eqid 2765	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))
84	46, 83	fmptd 6574	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
85	84	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
86		eqid 2765	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))
87	47, 86	fmptd 6574	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
88	87	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
89		hoidmv1le.s	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
90	5	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ 𝑋 ↔ 𝑘 ∈ {𝑍})
91	90	biimpi 207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ {𝑍})
92		elsni 4351	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑋 → 𝑘 = 𝑍)
94	93, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑋 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
95	94	rgen 3069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
96		ixpeq2 8127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
98	97	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
99	98	iuneq2i 4695	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
100	99	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
101	89, 100	sseqtrd 3801	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
102	101	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
103		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
104		eqidd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105		opeq2 4560	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106	105	sneqd 4346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107	106	rspceeqv 3479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108	103, 104, 107	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109	108	adantl 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110		elixpsn 8152	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
111	2, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112	111	adantr 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113	109, 112	mpbird 248	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
114	5	eqcomi 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑍} = 𝑋
115		ixpeq1 8124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑍} = 𝑋 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
116	114, 115	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍))
117		fveq2 6375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍))
118	93, 117	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑋 → (𝐴‘𝑘) = (𝐴‘𝑍))
119		fveq2 6375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍))
120	93, 119	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑋 → (𝐵‘𝑘) = (𝐵‘𝑍))
121	118, 120	oveq12d 6860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑋 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
122	121	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑋 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
123	122	rgen 3069	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))
124		ixpeq2 8127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
126	116, 125	eqtri 2787	. . . . . . . . . . . . . . . . . 18 ⊢ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
127	126	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
128	127	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
129	113, 128	eleqtrd 2846	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
130	102, 129	sseldd 3762	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
131		eliun 4680	. . . . . . . . . . . . . 14 ⊢ ({⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
132	130, 131	sylib 209	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
133		ixpeq1 8124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = {𝑍} → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
134	5, 133	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
135	134	eleq2i 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
136	135	biimpi 207	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
137	136	adantl 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
138		elixpsn 8152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
139	2, 138	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140	139	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
141	137, 140	mpbid 223	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
142		opex 5088	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⟨𝑍, 𝑥⟩ ∈ V
143	142	sneqr 4523	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144	143	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
145		vex 3353	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑥 ∈ V
146	145	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑥 ∈ V)
147		opthg 5101	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
148	2, 146, 147	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
149	148	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
150	144, 149	mpbid 223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))
151	150	simprd 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
152	151	3adant2 1161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
153		simp2 1167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
154	152, 153	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
155	154	3exp 1148	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
156	155	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
157	156	rexlimdv 3177	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
158	141, 157	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
159	158	ex 401	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
160	159	ad2antrr 717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
161	160	reximdva 3163	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
162	132, 161	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
163		eliun 4680	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
164	162, 163	sylibr 225	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → 𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
165	164	ralrimiva 3113	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
166		dfss3 3750	. . . . . . . . . 10 ⊢ (((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
167	165, 166	sylibr 225	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
168		eqidd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)))
169		fveq2 6375	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
170	169	fveq1d 6377	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
171	170	adantl 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
172		simpr 477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
173		fvexd 6390	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ V)
174	168, 171, 172, 173	fvmptd 6477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
175		eqidd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)))
176		fveq2 6375	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
177	176	fveq1d 6377	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
178	177	adantl 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
179		fvexd 6390	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ V)
180	175, 178, 172, 179	fvmptd 6477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
181	174, 180	oveq12d 6860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
182	181	iuneq2dv 4698	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
183	170, 177	oveq12d 6860	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
184	183	cbviunv 4715	. . . . . . . . . . . 12 ⊢ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))
185	184	eqcomi 2774	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
186	185	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
187	182, 186	eqtr2d 2800	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
188	167, 187	sseqtrd 3801	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
189	188	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
190		fvex 6388	. . . . . . . . . . . . . . 15 ⊢ ((𝐶‘𝑖)‘𝑍) ∈ V
191	170, 83, 190	fvmpt 6471	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
192		fvex 6388	. . . . . . . . . . . . . . 15 ⊢ ((𝐷‘𝑖)‘𝑍) ∈ V
193	177, 86, 192	fvmpt 6471	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
194	191, 193	oveq12d 6860	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
195	194	fveq2d 6379	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
196	195	mpteq2ia 4899	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
197		eqcom 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 ↔ 𝑖 = 𝑗)
198	197	imbi1i 340	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
199		eqcom 2772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) ↔ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
200	199	imbi2i 327	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
201	198, 200	bitri 266	. . . . . . . . . . . . . 14 ⊢ ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
202	183, 201	mpbi 221	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
203	202	fveq2d 6379	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
204	203	cbvmptv 4909	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
205	196, 204	eqtri 2787	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
206	205	fveq2i 6378	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
207	206	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
208		simpr 477	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
209	207, 208	eqeltrd 2844	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
210		oveq1 6849	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
211	193	breq1d 4819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷‘𝑖)‘𝑍) ≤ 𝑧))
212	211, 193	ifbieq1d 4266	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))
213	191, 212	oveq12d 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))
214	213	fveq2d 6379	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
215	214	mpteq2ia 4899	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
216		fveq2 6375	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = ℎ → (𝐶‘𝑖) = (𝐶‘ℎ))
217	216	fveq1d 6377	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → ((𝐶‘𝑖)‘𝑍) = ((𝐶‘ℎ)‘𝑍))
218		fveq2 6375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = ℎ → (𝐷‘𝑖) = (𝐷‘ℎ))
219	218	fveq1d 6377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = ℎ → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘ℎ)‘𝑍))
220	219	breq1d 4819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = ℎ → (((𝐷‘𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
221	220, 219	ifbieq1d 4266	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
222	217, 221	oveq12d 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ℎ → (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))
223	222	fveq2d 6379	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ℎ → (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
224	223	cbvmptv 4909	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
225	215, 224	eqtri 2787	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
226	225	a1i 11	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))))
227		breq2 4813	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (((𝐷‘ℎ)‘𝑍) ≤ 𝑤 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
228		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
229	227, 228	ifbieq2d 4268	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
230	229	eqcomd 2771	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))
231	230	oveq2d 6858	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))
232	231	fveq2d 6379	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))
233	232	mpteq2dv 4904	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))
234	226, 233	eqtr2d 2800	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))
235	234	fveq2d 6379	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (Σ^{^}‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) = (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))))
236	210, 235	breq12d 4822	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → ((𝑤 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))))
237	236	cbvrabv 3348	. . . . . . 7 ⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))}
238		eqid 2765	. . . . . . 7 ⊢ sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^{^}‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < )
239	80, 81, 82, 85, 88, 189, 209, 237, 238	hoidmv1lelem3 41379	. . . . . 6 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))))
240	239, 207	breqtrd 4835	. . . . 5 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
241	21, 79, 240	syl2anc 579	. . . 4 ⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
242	20, 241	pm2.61dan 847	. . 3 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
243	25, 29, 31, 8, 1	hoidmvn0val 41370	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
244	26	prodeq1d 14936	. . . . . . 7 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
245		volicore 41367	. . . . . . . . . 10 ⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
246	9, 7, 245	syl2anc 579	. . . . . . . . 9 ⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
247	246	recnd 10322	. . . . . . . 8 ⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ)
248	117, 119	oveq12d 6860	. . . . . . . . . 10 ⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
249	248	fveq2d 6379	. . . . . . . . 9 ⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
250	249	prodsn 14977	. . . . . . . 8 ⊢ ((𝑍 ∈ 𝑉 ∧ (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
251	2, 247, 250	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
252	243, 244, 251	3eqtrd 2803	. . . . . 6 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
253	252	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
254		volico 40769	. . . . . . 7 ⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
255	9, 7, 254	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
256	255	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
257		iftrue 4249	. . . . . 6 ⊢ ((𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
258	257	adantl 473	. . . . 5 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
259	253, 256, 258	3eqtrd 2803	. . . 4 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
260	58	fveq2d 6379	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
261	260	adantr 472	. . . 4 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
262	259, 261	breq12d 4822	. . 3 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ↔ ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))))
263	242, 262	mpbird 248	. 2 ⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
264	243	adantr 472	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
265	244	adantr 472	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
266	251	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
267	255	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
268		iffalse 4252	. . . . . 6 ⊢ (¬ (𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
269	268	adantl 473	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
270	266, 267, 269	3eqtrd 2803	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
271	264, 265, 270	3eqtrd 2803	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
272	23	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ∈ V)
273	272, 75	sge0ge0 41170	. . . 4 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
274	273	adantr 472	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
275	271, 274	eqbrtrd 4831	. 2 ⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
276	263, 275	pm2.61dan 847	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∃wrex 3056 {crab 3059 Vcvv 3350 ⊆ wss 3732 ∅c0 4079 ifcif 4243 {csn 4334 ⟨cop 4340 ∪ ciun 4676 class class class wbr 4809 ↦ cmpt 4888 ⟶wf 6064 ‘cfv 6068 (class class class)co 6842 ↦ cmpt2 6844 ↑_𝑚 cmap 8060 Xcixp 8113 Fincfn 8160 supcsup 8553 ℂcc 10187 ℝcr 10188 0cc0 10189 +∞cpnf 10325 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329 − cmin 10520 ℕcn 11274 [,)cico 12379 [,]cicc 12380 ∏cprod 14920 volcvol 23521 Σ^{^}csumge0 41148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2069 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-inf2 8753 ax-cnex 10245 ax-resscn 10246 ax-1cn 10247 ax-icn 10248 ax-addcl 10249 ax-addrcl 10250 ax-mulcl 10251 ax-mulrcl 10252 ax-mulcom 10253 ax-addass 10254 ax-mulass 10255 ax-distr 10256 ax-i2m1 10257 ax-1ne0 10258 ax-1rid 10259 ax-rnegex 10260 ax-rrecex 10261 ax-cnre 10262 ax-pre-lttri 10263 ax-pre-lttrn 10264 ax-pre-ltadd 10265 ax-pre-mulgt0 10266 ax-pre-sup 10267

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-fal 1666 df-ex 1875 df-nf 1879 df-sb 2062 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-se 5237 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-isom 6077 df-riota 6803 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-of 7095 df-om 7264 df-1st 7366 df-2nd 7367 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-2o 7765 df-oadd 7768 df-er 7947 df-map 8062 df-pm 8063 df-ixp 8114 df-en 8161 df-dom 8162 df-sdom 8163 df-fin 8164 df-fi 8524 df-sup 8555 df-inf 8556 df-oi 8622 df-card 9016 df-cda 9243 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-sub 10522 df-neg 10523 df-div 10939 df-nn 11275 df-2 11335 df-3 11336 df-n0 11539 df-z 11625 df-uz 11887 df-q 11990 df-rp 12029 df-xneg 12146 df-xadd 12147 df-xmul 12148 df-ioo 12381 df-ico 12383 df-icc 12384 df-fz 12534 df-fzo 12674 df-fl 12801 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14126 df-re 14127 df-im 14128 df-sqrt 14262 df-abs 14263 df-clim 14506 df-rlim 14507 df-sum 14704 df-prod 14921 df-rest 16351 df-topgen 16372 df-psmet 20011 df-xmet 20012 df-met 20013 df-bl 20014 df-mopn 20015 df-top 20978 df-topon 20995 df-bases 21030 df-cmp 21470 df-ovol 23522 df-vol 23523 df-sumge0 41149

This theorem is referenced by: hoidmvle 41386

W3C validator