P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unmbl 24901	A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol)
Theorem	shftmbl 24902*	A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol)
Theorem	0mbl 24903	The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ∅ ∈ dom vol
Theorem	rembl 24904	The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ℝ ∈ dom vol
Theorem	unidmvol 24905	The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ∪ dom vol = ℝ
Theorem	inmbl 24906	An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol)
Theorem	difmbl 24907	A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol)
Theorem	finiunmbl 24908*	A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	volun 24909	The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)))
Theorem	volinun 24910	Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵))))
Theorem	volfiniun 24911*	The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧ Disj 𝑘 ∈ 𝐴 𝐵) → (vol‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (vol‘𝐵))
Theorem	iundisj 24912*	Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2 24913*	A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	voliunlem1 24914*	Lemma for voliun 24918. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛))))    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸))
Theorem	voliunlem2 24915*	Lemma for voliun 24918. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    ⇒   ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol)
Theorem	voliunlem3 24916*	Lemma for voliun 24918. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    &   ⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Theorem	iunmbl 24917	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol)
Theorem	voliun 24918	The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴))    ⇒   ⊢ ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, < ))
Theorem	volsuplem 24919*	Lemma for volsup 24920. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	volsup 24920*	The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
Theorem	iunmbl2 24921*	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	ioombl1lem1 24922*	Lemma for ioombl1 24926. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
Theorem	ioombl1lem2 24923*	Lemma for ioombl1 24926. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
Theorem	ioombl1lem3 24924*	Lemma for ioombl1 24926. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
Theorem	ioombl1lem4 24925*	Lemma for ioombl1 24926. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
Theorem	ioombl1 24926	An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴(,)+∞) ∈ dom vol)
Theorem	icombl1 24927	A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol)
Theorem	icombl 24928	A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol)
Theorem	ioombl 24929	An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴(,)𝐵) ∈ dom vol
Theorem	iccmbl 24930	A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
Theorem	iccvolcl 24931	A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)
Theorem	ovolioo 24932	The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	volioo 24933	The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	ioovolcl 24934	An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
Theorem	ovolfs2 24935	Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹))
Theorem	ioorcl2 24936	An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
Theorem	ioorf 24937	Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ 𝐹:ran (,)⟶( ≤ ∩ (ℝ* × ℝ*))
Theorem	ioorval 24938*	Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ (𝐴 ∈ ran (,) → (𝐹‘𝐴) = if(𝐴 = ∅, ⟨0, 0⟩, ⟨inf(𝐴, ℝ*, < ), sup(𝐴, ℝ*, < )⟩))
Theorem	ioorinv2 24939*	The function 𝐹 is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐹‘(𝐴(,)𝐵)) = ⟨𝐴, 𝐵⟩)
Theorem	ioorinv 24940*	The function 𝐹 is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ (𝐴 ∈ ran (,) → ((,)‘(𝐹‘𝐴)) = 𝐴)
Theorem	ioorcl 24941*	The function 𝐹 does not always return real numbers, but it does on intervals of finite volume. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝐴 ∈ ran (,) ∧ (vol*‘𝐴) ∈ ℝ) → (𝐹‘𝐴) ∈ ( ≤ ∩ (ℝ × ℝ)))
Theorem	uniiccdif 24942	A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    ⇒   ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
Theorem	uniioovol 24943*	A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 24918.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Theorem	uniiccvol 24944*	An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 24918.) (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Theorem	uniioombllem1 24945*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
Theorem	uniioombllem2a 24946*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,))
Theorem	uniioombllem2 24947*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by AV, 13-Sep-2020.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))    &   ⊢ 𝐾 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , (vol* ∘ 𝐻)) ⇝ (vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴)))
Theorem	uniioombllem3a 24948*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
Theorem	uniioombllem3 24949*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
Theorem	uniioombllem4 24950*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))    &   ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))    ⇒   ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
Theorem	uniioombllem5 24951*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))    &   ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
Theorem	uniioombllem6 24952*	Lemma for uniioombl 24953. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
Theorem	uniioombl 24953*	A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24917.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol)
Theorem	uniiccmbl 24954*	An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24917.) (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ∈ dom vol)
Theorem	dyadf 24955*	The function 𝐹 returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ 𝐹:(ℤ × ℕ0)⟶( ≤ ∩ (ℝ × ℝ))
Theorem	dyadval 24956*	Value of the dyadic rational function 𝐹. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (𝐴𝐹𝐵) = ⟨(𝐴 / (2↑𝐵)), ((𝐴 + 1) / (2↑𝐵))⟩)
Theorem	dyadovol 24957*	Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (vol*‘([,]‘(𝐴𝐹𝐵))) = (1 / (2↑𝐵)))
Theorem	dyadss 24958*	Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) (Proof shortened by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) → 𝐷 ≤ 𝐶))
Theorem	dyaddisjlem 24959*	Lemma for dyaddisj 24960. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅))
Theorem	dyaddisj 24960*	Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹) → (([,]‘𝐴) ⊆ ([,]‘𝐵) ∨ ([,]‘𝐵) ⊆ ([,]‘𝐴) ∨ (((,)‘𝐴) ∩ ((,)‘𝐵)) = ∅))
Theorem	dyadmaxlem 24961*	Lemma for dyadmax 24962. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ 𝐷 < 𝐶)    &   ⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))
Theorem	dyadmax 24962*	Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → ∃𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤))
Theorem	dyadmbllem 24963*	Lemma for dyadmbl 24964. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)}    &   ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)    ⇒   ⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,] “ 𝐺))
Theorem	dyadmbl 24964*	Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)}    &   ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)    ⇒   ⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol)
Theorem	opnmbllem 24965*	Lemma for opnmbl 24966. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	opnmbl 24966	All open sets are measurable. This proof, via dyadmbl 24964 and uniioombl 24953, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	opnmblALT 24967	All open sets are measurable. This alternative proof of opnmbl 24966 is significantly shorter, at the expense of invoking countable choice ax-cc 10371. (This was also the original proof before the current opnmbl 24966 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	subopnmbl 24968	Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ 𝐽) → 𝐵 ∈ dom vol)
Theorem	volsup2 24969*	The volume of 𝐴 is the supremum of the sequence vol*‘(𝐴 ∩ (-𝑛[,]𝑛)) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
Theorem	volcn 24970*	The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥))))    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ))
Theorem	volivth 24971*	The Intermediate Value Theorem for the Lebesgue volume function. For any positive 𝐵 ≤ (vol‘𝐴), there is a measurable subset of 𝐴 whose volume is 𝐵. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
Theorem	vitalilem1 24972*	Lemma for vitali 24977. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    ⇒   ⊢ ∼ Er (0[,]1)
Theorem	vitalilem2 24973*	Lemma for vitali 24977. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)))
Theorem	vitalilem3 24974*	Lemma for vitali 24977. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))
Theorem	vitalilem4 24975*	Lemma for vitali 24977. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0)
Theorem	vitalilem5 24976*	Lemma for vitali 24977. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ ¬ 𝜑
Theorem	vitali 24977	If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ( < We ℝ → dom vol ⊊ 𝒫 ℝ)
13.2.2  Lebesgue integration
13.2.2.1  Lesbesgue integral
Syntax	cmbf 24978	Extend class notation with the class of measurable functions.
class MblFn
Syntax	citg1 24979	Extend class notation with the Lebesgue integral for simple functions.
class ∫1
Syntax	citg2 24980	Extend class notation with the Lebesgue integral for nonnegative functions.
class ∫2
Syntax	cibl 24981	Extend class notation with the class of integrable functions.
class 𝐿1
Syntax	citg 24982	Extend class notation with the general Lebesgue integral.
class ∫𝐴𝐵 d𝑥
Definition	df-mbf 24983*	Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 24890) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Definition	df-itg1 24984*	Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
Definition	df-itg2 24985*	Define the Lebesgue integral for nonnegative functions. A nonnegative function's integral is the supremum of the integrals of all simple functions that are less than the input function. Note that this may be +∞ for functions that take the value +∞ on a set of positive measure or functions that are bounded below by a positive number on a set of infinite measure. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < ))
Definition	df-ibl 24986*	Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
Definition	df-itg 24987*	Define the full Lebesgue integral, for complex-valued functions to ℝ. The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of 𝑥↑2 from 0 to 1 is ∫(0[,]1)(𝑥↑2) d𝑥 = (1 / 3). The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 24985 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 24985 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
Theorem	ismbf1 24988*	The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 24992 and ismbfcn 24993 for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
Theorem	mbff 24989	A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
Theorem	mbfdm 24990	The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
Theorem	mbfconstlem 24991	Lemma for mbfconst 24997 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ) → (◡(𝐴 × {𝐶}) “ 𝐵) ∈ dom vol)
Theorem	ismbf 24992*	The predicate "𝐹 is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl 24890. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
Theorem	ismbfcn 24993	A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
Theorem	mbfima 24994	Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝐵(,)𝐶)) ∈ dom vol)
Theorem	mbfimaicc 24995	The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (◡𝐹 “ (𝐵[,]𝐶)) ∈ dom vol)
Theorem	mbfimasn 24996	The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ ∧ 𝐵 ∈ ℝ) → (◡𝐹 “ {𝐵}) ∈ dom vol)
Theorem	mbfconst 24997	A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn)
Theorem	mbf0 24998	The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.)
⊢ ∅ ∈ MblFn
Theorem	mbfid 24999	The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn)
Theorem	mbfmptcl 25000*	Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)