hspmbl - Mathbox for Glauco Siliprandi

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

Theorem hspmbl 40843

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)

**Hypotheses**
Ref	Expression
hspmbl.1	⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
hspmbl.x	⊢ (𝜑 → 𝑋 ∈ Fin)
hspmbl.i	⊢ (𝜑 → 𝐾 ∈ 𝑋)
hspmbl.y	⊢ (𝜑 → 𝑌 ∈ ℝ)

**Assertion**
Ref	Expression
hspmbl	⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ dom (voln‘𝑋))

Distinct variable groups: 𝑥,𝑘 𝐾,𝑙,𝑥,𝑦 𝑋,𝑙,𝑥,𝑦 𝑌,𝑙,𝑥,𝑦 𝜑,𝑙 𝑘,𝑙,𝑦 𝜑,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑘) 𝐻(𝑥,𝑦,𝑘,𝑙) 𝐾(𝑘) 𝑋(𝑘) 𝑌(𝑘)

Proof of Theorem hspmbl Dummy variables 𝑎 𝑗 𝑝 𝑡 𝑏 ℎ 𝑐 𝑟 𝑠 𝑖 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hspmbl.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ Fin)
2	1	ovnome 40787	. . 3 ⊢ (𝜑 → (voln*‘𝑋) ∈ OutMeas)
3		eqid 2622	. . 3 ⊢ ∪ dom (voln‘𝑋) = ∪ dom (voln‘𝑋)
4		eqid 2622	. . 3 ⊢ (CaraGen‘(voln‘𝑋)) = (CaraGen‘(voln‘𝑋))
5		ovex 6678	. . . . . . . . 9 ⊢ (-∞(,)𝑌) ∈ V
6		reex 10027	. . . . . . . . 9 ⊢ ℝ ∈ V
7	5, 6	ifex 4156	. . . . . . . 8 ⊢ if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V
8	7	ixpssmap 7942	. . . . . . 7 ⊢ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ (∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ↑_𝑚 𝑋)
9		iftrue 4092	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐾 → if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
10		ioossre 12235	. . . . . . . . . . . . 13 ⊢ (-∞(,)𝑌) ⊆ ℝ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
12	9, 11	eqsstrd 3639	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐾 → if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
13		iffalse 4095	. . . . . . . . . . . 12 ⊢ (¬ 𝑝 = 𝐾 → if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
14		ssid 3624	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℝ
15	14	a1i 11	. . . . . . . . . . . 12 ⊢ (¬ 𝑝 = 𝐾 → ℝ ⊆ ℝ)
16	13, 15	eqsstrd 3639	. . . . . . . . . . 11 ⊢ (¬ 𝑝 = 𝐾 → if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
17	12, 16	pm2.61i 176	. . . . . . . . . 10 ⊢ if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
18	17	rgenw 2924	. . . . . . . . 9 ⊢ ∀𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
19		iunss 4561	. . . . . . . . 9 ⊢ (∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ ↔ ∀𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
20	18, 19	mpbir 221	. . . . . . . 8 ⊢ ∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
21		mapss 7900	. . . . . . . 8 ⊢ ((ℝ ∈ V ∧ ∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ) → (∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ↑_𝑚 𝑋) ⊆ (ℝ ↑_𝑚 𝑋))
22	6, 20, 21	mp2an 708	. . . . . . 7 ⊢ (∪ 𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ↑_𝑚 𝑋) ⊆ (ℝ ↑_𝑚 𝑋)
23	8, 22	sstri 3612	. . . . . 6 ⊢ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ (ℝ ↑_𝑚 𝑋)
24	7	rgenw 2924	. . . . . . . 8 ⊢ ∀𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V
25		ixpexg 7932	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V → X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V)
26	24, 25	ax-mp 5	. . . . . . 7 ⊢ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V
27		elpwg 4166	. . . . . . 7 ⊢ (X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ V → (X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↔ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ (ℝ ↑_𝑚 𝑋)))
28	26, 27	ax-mp 5	. . . . . 6 ⊢ (X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↔ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ (ℝ ↑_𝑚 𝑋))
29	23, 28	mpbir 221	. . . . 5 ⊢ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ 𝒫 (ℝ ↑_𝑚 𝑋)
30	29	a1i 11	. . . 4 ⊢ (𝜑 → X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ 𝒫 (ℝ ↑_𝑚 𝑋))
31		hspmbl.1	. . . . . . 7 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
32		equid 1939	. . . . . . . . 9 ⊢ 𝑥 = 𝑥
33		eqid 2622	. . . . . . . . 9 ⊢ ℝ = ℝ
34		equequ1 1952	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑝 → (𝑘 = 𝑙 ↔ 𝑝 = 𝑙))
35	34	ifbid 4108	. . . . . . . . . 10 ⊢ (𝑘 = 𝑝 → if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑝 = 𝑙, (-∞(,)𝑦), ℝ))
36	35	cbvixpv 7926	. . . . . . . . 9 ⊢ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑝 ∈ 𝑥 if(𝑝 = 𝑙, (-∞(,)𝑦), ℝ)
37	32, 33, 36	mpt2eq123i 6718	. . . . . . . 8 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑝 ∈ 𝑥 if(𝑝 = 𝑙, (-∞(,)𝑦), ℝ))
38	37	mpteq2i 4741	. . . . . . 7 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑝 ∈ 𝑥 if(𝑝 = 𝑙, (-∞(,)𝑦), ℝ)))
39	31, 38	eqtri 2644	. . . . . 6 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑝 ∈ 𝑥 if(𝑝 = 𝑙, (-∞(,)𝑦), ℝ)))
40		hspmbl.i	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
41		hspmbl.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
42	39, 1, 40, 41	hspval 40823	. . . . 5 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ))
43	1	ovnf 40777	. . . . . . . . 9 ⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑_𝑚 𝑋)⟶(0[,]+∞))
44		fdm 6051	. . . . . . . . 9 ⊢ ((voln‘𝑋):𝒫 (ℝ ↑_𝑚 𝑋)⟶(0[,]+∞) → dom (voln‘𝑋) = 𝒫 (ℝ ↑_𝑚 𝑋))
45	43, 44	syl 17	. . . . . . . 8 ⊢ (𝜑 → dom (voln*‘𝑋) = 𝒫 (ℝ ↑_𝑚 𝑋))
46	45	unieqd 4446	. . . . . . 7 ⊢ (𝜑 → ∪ dom (voln*‘𝑋) = ∪ 𝒫 (ℝ ↑_𝑚 𝑋))
47		unipw 4918	. . . . . . . 8 ⊢ ∪ 𝒫 (ℝ ↑_𝑚 𝑋) = (ℝ ↑_𝑚 𝑋)
48	47	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝒫 (ℝ ↑_𝑚 𝑋) = (ℝ ↑_𝑚 𝑋))
49	46, 48	eqtrd 2656	. . . . . 6 ⊢ (𝜑 → ∪ dom (voln*‘𝑋) = (ℝ ↑_𝑚 𝑋))
50	49	pweqd 4163	. . . . 5 ⊢ (𝜑 → 𝒫 ∪ dom (voln*‘𝑋) = 𝒫 (ℝ ↑_𝑚 𝑋))
51	42, 50	eleq12d 2695	. . . 4 ⊢ (𝜑 → ((𝐾(𝐻‘𝑋)𝑌) ∈ 𝒫 ∪ dom (voln*‘𝑋) ↔ X𝑝 ∈ 𝑋 if(𝑝 = 𝐾, (-∞(,)𝑌), ℝ) ∈ 𝒫 (ℝ ↑_𝑚 𝑋)))
52	30, 51	mpbird 247	. . 3 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ 𝒫 ∪ dom (voln*‘𝑋))
53		simpl 473	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom (voln*‘𝑋)) → 𝜑)
54		simpr 477	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom (voln‘𝑋)) → 𝑎 ∈ 𝒫 ∪ dom (voln‘𝑋))
55	53, 50	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom (voln‘𝑋)) → 𝒫 ∪ dom (voln‘𝑋) = 𝒫 (ℝ ↑_𝑚 𝑋))
56	54, 55	eleqtrd 2703	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom (voln*‘𝑋)) → 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋))
57	1	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → 𝑋 ∈ Fin)
58		inss1 3833	. . . . . . . . . . . . 13 ⊢ (𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ 𝑎
59	58	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) → (𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ 𝑎)
60		elpwi 4168	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) → 𝑎 ⊆ (ℝ ↑_𝑚 𝑋))
61	59, 60	sstrd 3613	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) → (𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ (ℝ ↑_𝑚 𝑋))
62	61	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → (𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ (ℝ ↑_𝑚 𝑋))
63	57, 62	ovnxrcl 40783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → ((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ^)
64	60	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → 𝑎 ⊆ (ℝ ↑_𝑚 𝑋))
65	64	ssdifssd 3748	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → (𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ (ℝ ↑_𝑚 𝑋))
66	57, 65	ovnxrcl 40783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ^)
67	63, 66	xaddcld 12131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ^*)
68		pnfge 11964	. . . . . . . 8 ⊢ ((((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ^* → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ +∞)
69	67, 68	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ +∞)
70	69	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln‘𝑋)‘𝑎) = +∞) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln*‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ +∞)
71		id 22	. . . . . . . 8 ⊢ (((voln‘𝑋)‘𝑎) = +∞ → ((voln‘𝑋)‘𝑎) = +∞)
72	71	eqcomd 2628	. . . . . . 7 ⊢ (((voln‘𝑋)‘𝑎) = +∞ → +∞ = ((voln‘𝑋)‘𝑎))
73	72	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln‘𝑋)‘𝑎) = +∞) → +∞ = ((voln‘𝑋)‘𝑎))
74	70, 73	breqtrd 4679	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln‘𝑋)‘𝑎) = +∞) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln‘𝑋)‘𝑎))
75		simpl 473	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ¬ ((voln*‘𝑋)‘𝑎) = +∞) → (𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)))
76	57, 64	ovncl 40781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → ((voln*‘𝑋)‘𝑎) ∈ (0[,]+∞))
77	76	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ¬ ((voln‘𝑋)‘𝑎) = +∞) → ((voln‘𝑋)‘𝑎) ∈ (0[,]+∞))
78		neqne 2802	. . . . . . . 8 ⊢ (¬ ((voln‘𝑋)‘𝑎) = +∞ → ((voln‘𝑋)‘𝑎) ≠ +∞)
79	78	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ¬ ((voln‘𝑋)‘𝑎) = +∞) → ((voln‘𝑋)‘𝑎) ≠ +∞)
80		ge0xrre 39758	. . . . . . 7 ⊢ ((((voln‘𝑋)‘𝑎) ∈ (0[,]+∞) ∧ ((voln‘𝑋)‘𝑎) ≠ +∞) → ((voln*‘𝑋)‘𝑎) ∈ ℝ)
81	77, 79, 80	syl2anc 693	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ¬ ((voln‘𝑋)‘𝑎) = +∞) → ((voln‘𝑋)‘𝑎) ∈ ℝ)
82	57	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln*‘𝑋)‘𝑎) ∈ ℝ) → 𝑋 ∈ Fin)
83	40	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln*‘𝑋)‘𝑎) ∈ ℝ) → 𝐾 ∈ 𝑋)
84	41	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln*‘𝑋)‘𝑎) ∈ ℝ) → 𝑌 ∈ ℝ)
85		simpr 477	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln‘𝑋)‘𝑎) ∈ ℝ) → ((voln‘𝑋)‘𝑎) ∈ ℝ)
86	64	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln*‘𝑋)‘𝑎) ∈ ℝ) → 𝑎 ⊆ (ℝ ↑_𝑚 𝑋))
87		sseq1 3626	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝) ↔ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)))
88	87	rabbidv 3189	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)} = {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})
89	88	cbvmptv 4750	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)}) = (𝑏 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})
90		simpl 473	. . . . . . . . . . . 12 ⊢ ((𝑖 = ℎ ∧ 𝑝 ∈ 𝑋) → 𝑖 = ℎ)
91	90	coeq2d 5284	. . . . . . . . . . 11 ⊢ ((𝑖 = ℎ ∧ 𝑝 ∈ 𝑋) → ([,) ∘ 𝑖) = ([,) ∘ ℎ))
92	91	fveq1d 6193	. . . . . . . . . 10 ⊢ ((𝑖 = ℎ ∧ 𝑝 ∈ 𝑋) → (([,) ∘ 𝑖)‘𝑝) = (([,) ∘ ℎ)‘𝑝))
93	92	fveq2d 6195	. . . . . . . . 9 ⊢ ((𝑖 = ℎ ∧ 𝑝 ∈ 𝑋) → (vol‘(([,) ∘ 𝑖)‘𝑝)) = (vol‘(([,) ∘ ℎ)‘𝑝)))
94	93	prodeq2dv 14653	. . . . . . . 8 ⊢ (𝑖 = ℎ → ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)) = ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑝)))
95	94	cbvmptv 4750	. . . . . . 7 ⊢ (𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝))) = (ℎ ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑝)))
96		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑝 → (([,) ∘ (𝑚‘𝑖))‘𝑛) = (([,) ∘ (𝑚‘𝑖))‘𝑝))
97	96	cbvixpv 7926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) = X𝑝 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑝)
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = ℎ → X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) = X𝑝 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑝))
99		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = ℎ → (𝑚‘𝑖) = (ℎ‘𝑖))
100	99	coeq2d 5284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = ℎ → ([,) ∘ (𝑚‘𝑖)) = ([,) ∘ (ℎ‘𝑖)))
101	100	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = ℎ → (([,) ∘ (𝑚‘𝑖))‘𝑝) = (([,) ∘ (ℎ‘𝑖))‘𝑝))
102	101	ixpeq2dv 7924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = ℎ → X𝑝 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑝) = X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝))
103	98, 102	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = ℎ → X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) = X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝))
104	103	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = ℎ ∧ 𝑖 ∈ ℕ) → X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) = X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝))
105	104	iuneq2dv 4542	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = ℎ → ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) = ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝))
106	105	sseq2d 3633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = ℎ → (𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛) ↔ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝)))
107	106	cbvrabv 3199	. . . . . . . . . . . . . . . . 17 ⊢ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)} = {ℎ ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝)}
108		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 𝑙 → (ℎ‘𝑖) = (𝑙‘𝑖))
109	108	coeq2d 5284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑙 → ([,) ∘ (ℎ‘𝑖)) = ([,) ∘ (𝑙‘𝑖)))
110	109	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑙 → (([,) ∘ (ℎ‘𝑖))‘𝑝) = (([,) ∘ (𝑙‘𝑖))‘𝑝))
111	110	ixpeq2dv 7924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑙 → X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝) = X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝))
112	111	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ = 𝑙 ∧ 𝑖 ∈ ℕ) → X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝) = X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝))
113	112	iuneq2dv 4542	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝) = ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝))
114		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑙‘𝑖) = (𝑙‘𝑗))
115	114	coeq2d 5284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ([,) ∘ (𝑙‘𝑖)) = ([,) ∘ (𝑙‘𝑗)))
116	115	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (([,) ∘ (𝑙‘𝑖))‘𝑝) = (([,) ∘ (𝑙‘𝑗))‘𝑝))
117	116	ixpeq2dv 7924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝) = X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝))
118	117	cbviunv 4559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝) = ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑖))‘𝑝) = ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝))
120	113, 119	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝) = ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝))
121	120	sseq2d 3633	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑙 → (𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝) ↔ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)))
122	121	cbvrabv 3199	. . . . . . . . . . . . . . . . 17 ⊢ {ℎ ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (ℎ‘𝑖))‘𝑝)} = {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)}
123	107, 122	eqtri 2644	. . . . . . . . . . . . . . . 16 ⊢ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)} = {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)}
124	123	mpteq2i 4741	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)}) = (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})
125	124	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)}) = (𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)}))
126		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → 𝑐 = 𝑏)
127	125, 126	fveq12d 6197	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) = ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏))
128	127	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ↔ 𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏)))
129		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑝 → (([,) ∘ 𝑖)‘𝑚) = (([,) ∘ 𝑖)‘𝑝))
130	129	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑝 → (vol‘(([,) ∘ 𝑖)‘𝑚)) = (vol‘(([,) ∘ 𝑖)‘𝑝)))
131	130	cbvprodv 14646	. . . . . . . . . . . . . . . . . . 19 ⊢ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)) = ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝))
132	131	mpteq2i 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚))) = (𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))
133	132	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → (𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚))) = (𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝))))
134		fveq2 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → (𝑡‘𝑚) = (𝑡‘𝑗))
135	133, 134	fveq12d 6197	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)) = ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))
136	135	cbvmptv 4750	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚))) = (𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))
137	136	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → (𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚))) = (𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗))))
138	137	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))))
139		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((voln‘𝑋)‘𝑐) = ((voln‘𝑋)‘𝑏))
140	139	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (((voln‘𝑋)‘𝑐) +_𝑒 𝑠) = (((voln‘𝑋)‘𝑏) +_𝑒 𝑠))
141	138, 140	breq12d 4666	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → ((Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠) ↔ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)))
142	128, 141	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑏 → ((𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ∧ (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠)) ↔ (𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠))))
143	142	rabbidva2 3186	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ∣ (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠)} = {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)})
144	143	mpteq2dv 4745	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ∣ (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠)}) = (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)}))
145		eqidd 2623	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑟 → ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) = ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏))
146	145	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑟 → (𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ↔ 𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏)))
147		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑟 → (((voln‘𝑋)‘𝑏) +_𝑒 𝑠) = (((voln‘𝑋)‘𝑏) +_𝑒 𝑟))
148	147	breq2d 4665	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑟 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠) ↔ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)))
149	146, 148	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑟 → ((𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)) ↔ (𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟))))
150	149	rabbidva2 3186	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑟 → {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)} = {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)})
151	150	cbvmptv 4750	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)})
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑠)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)}))
153	144, 152	eqtrd 2656	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ∣ (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)}))
154	153	cbvmptv 4750	. . . . . . 7 ⊢ (𝑐 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ (𝑠 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑚 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X𝑛 ∈ 𝑋 (([,) ∘ (𝑚‘𝑖))‘𝑛)})‘𝑐) ∣ (Σ^{^}‘(𝑚 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑚 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑚)))‘(𝑡‘𝑚)))) ≤ (((voln‘𝑋)‘𝑐) +_𝑒 𝑠)})) = (𝑏 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ (𝑟 ∈ ℝ⁺ ↦ {𝑡 ∈ ((𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑_𝑚 𝑋) ↑_𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑝 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑝)})‘𝑏) ∣ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑖 ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) ↦ ∏𝑝 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑝)))‘(𝑡‘𝑗)))) ≤ (((voln‘𝑋)‘𝑏) +_𝑒 𝑟)}))
155		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑚 = 𝑝 → ((𝑡‘𝑗)‘𝑚) = ((𝑡‘𝑗)‘𝑝))
156	155	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑚 = 𝑝 → (1^st ‘((𝑡‘𝑗)‘𝑚)) = (1^st ‘((𝑡‘𝑗)‘𝑝)))
157	156	cbvmptv 4750	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑋 ↦ (1^st ‘((𝑡‘𝑗)‘𝑚))) = (𝑝 ∈ 𝑋 ↦ (1^st ‘((𝑡‘𝑗)‘𝑝)))
158	157	mpteq2i 4741	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (𝑚 ∈ 𝑋 ↦ (1^st ‘((𝑡‘𝑗)‘𝑚)))) = (𝑗 ∈ ℕ ↦ (𝑝 ∈ 𝑋 ↦ (1^st ‘((𝑡‘𝑗)‘𝑝))))
159		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑡‘𝑖) = (𝑡‘𝑗))
160	159	fveq1d 6193	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑡‘𝑖)‘𝑚) = ((𝑡‘𝑗)‘𝑚))
161	160	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (2^nd ‘((𝑡‘𝑖)‘𝑚)) = (2^nd ‘((𝑡‘𝑗)‘𝑚)))
162	161	mpteq2dv 4745	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑖)‘𝑚))) = (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑚))))
163	155	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑝 → (2^nd ‘((𝑡‘𝑗)‘𝑚)) = (2^nd ‘((𝑡‘𝑗)‘𝑝)))
164	163	cbvmptv 4750	. . . . . . . . . 10 ⊢ (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑚))) = (𝑝 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑝)))
165	164	a1i 11	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑚))) = (𝑝 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑝))))
166	162, 165	eqtrd 2656	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑖)‘𝑚))) = (𝑝 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑝))))
167	166	cbvmptv 4750	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ (𝑚 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑖)‘𝑚)))) = (𝑗 ∈ ℕ ↦ (𝑝 ∈ 𝑋 ↦ (2^nd ‘((𝑡‘𝑗)‘𝑝))))
168	39, 82, 83, 84, 85, 86, 89, 95, 154, 158, 167	hspmbllem3 40842	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ((voln‘𝑋)‘𝑎) ∈ ℝ) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln‘𝑋)‘𝑎))
169	75, 81, 168	syl2anc 693	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) ∧ ¬ ((voln‘𝑋)‘𝑎) = +∞) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln‘𝑋)‘𝑎))
170	74, 169	pm2.61dan 832	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 (ℝ ↑_𝑚 𝑋)) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝑎))
171	53, 56, 170	syl2anc 693	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom (voln‘𝑋)) → (((voln‘𝑋)‘(𝑎 ∩ (𝐾(𝐻‘𝑋)𝑌))) +_𝑒 ((voln‘𝑋)‘(𝑎 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln‘𝑋)‘𝑎))
172	2, 3, 4, 52, 171	caragenel2d 40746	. 2 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ (CaraGen‘(voln*‘𝑋)))
173	1	dmvon 40820	. . 3 ⊢ (𝜑 → dom (voln‘𝑋) = (CaraGen‘(voln*‘𝑋)))
174	173	eqcomd 2628	. 2 ⊢ (𝜑 → (CaraGen‘(voln*‘𝑋)) = dom (voln‘𝑋))
175	172, 174	eleqtrd 2703	1 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ dom (voln‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∩ cin 3573 ⊆ wss 3574 ifcif 4086 𝒫 cpw 4158 ∪ cuni 4436 ∪ ciun 4520 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 dom cdm 5114 ∘ ccom 5118 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 1^st c1st 7166 2^nd c2nd 7167 ↑_𝑚 cmap 7857 Xcixp 7908 Fincfn 7955 ℝcr 9935 0cc0 9936 +∞cpnf 10071 -∞cmnf 10072 ℝ^*cxr 10073 ≤ cle 10075 ℕcn 11020 ℝ⁺crp 11832 +_𝑒 cxad 11944 (,)cioo 12175 [,)cico 12177 [,]cicc 12178 ∏cprod 14635 volcvol 23232 Σ^{^}csumge0 40579 CaraGenccaragen 40705 voln*covoln 40750 volncvoln 40752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cc 9257 ax-ac2 9285 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-ac 8939 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-rest 16083 df-0g 16102 df-topgen 16104 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-grp 17425 df-minusg 17426 df-subg 17591 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-drng 18749 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-sumge0 40580 df-ome 40704 df-caragen 40706 df-ovoln 40751 df-voln 40753

This theorem is referenced by: hoimbllem 40844

W3C validator