P. 320 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31901-32000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	esumeq12d 31901*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷)
Theorem	esumeq1 31902*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq1d 31903	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumeq2 31904*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2d 31905	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2dv 31906*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumeq2sdv 31907*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	nfesum1 31908	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵
Theorem	nfesum2 31909*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵
Theorem	cbvesum 31910*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	cbvesumv 31911*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶
Theorem	esumid 31912	Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = 𝐶)
Theorem	esumgsum 31913	A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	esumval 31914*	Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < ))
Theorem	esumel 31915*	The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	esumnul 31916	Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.)
⊢ Σ*𝑥 ∈ ∅𝐴 = 0
Theorem	esum0 31917*	Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0)
Theorem	esumf1o 31918*	Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ Ⅎ𝑛𝐶    &   ⊢ Ⅎ𝑛𝐹    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷)
Theorem	esumc 31919*	Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑘𝐷    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷)
Theorem	esumrnmpt 31920*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ Ⅎ𝑘𝐴    &   ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (𝑊 ∖ {∅}))    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐷)
Theorem	esumsplit 31921	Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶))
Theorem	esummono 31922*	Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵)
Theorem	esumpad 31923*	Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumpad2 31924*	Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumadd 31925*	Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumle 31926*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐴𝐶)
Theorem	gsumesum 31927*	Relate a group sum on (ℝ*𝑠 ↾s (0[,]+∞)) to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ*𝑘 ∈ 𝐴𝐵)
Theorem	esumlub 31928*	The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑋 < Σ*𝑘 ∈ 𝐴𝐵)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 < Σ*𝑘 ∈ 𝑎𝐵)
Theorem	esumaddf 31929*	Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶))
Theorem	esumlef 31930*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐴𝐶)
Theorem	esumcst 31931*	The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 = ((♯‘𝐴) ·e 𝐵))
Theorem	esumsnf 31932*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	esumsn 31933*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Shortened by Thierry Arnoux, 2-May-2020.)
⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	esumpr 31934*	Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸))
Theorem	esumpr2 31935*	Extended sum over a pair, with a relaxed condition compared to esumpr 31934. (Contributed by Thierry Arnoux, 2-Jan-2017.)
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (𝐴 = 𝐵 → (𝐷 = 0 ∨ 𝐷 = +∞)))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸))
Theorem	esumrnmpt2 31936*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐷)
Theorem	esumfzf 31937*	Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑁 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑁)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑁))
Theorem	esumfsup 31938	Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ))
Theorem	esumfsupre 31939	Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real-valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017.)
⊢ Ⅎ𝑘𝐹    ⇒   ⊢ (𝐹:ℕ⟶(0[,)+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( + , 𝐹), ℝ*, < ))
Theorem	esumss 31940	Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)
Theorem	esumpinfval 31941*	The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → ∃𝑘 ∈ 𝐴 𝐵 = +∞)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = +∞)
Theorem	esumpfinvallem 31942	Lemma for esumpfinval 31943. (Contributed by Thierry Arnoux, 28-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → (ℂfld Σg 𝐹) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg 𝐹))
Theorem	esumpfinval 31943*	The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017.) (Proof shortened by AV, 25-Jul-2019.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	esumpfinvalf 31944	Same as esumpfinval 31943, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	esumpinfsum 31945*	The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑀 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ*)    &   ⊢ (𝜑 → 0 < 𝑀)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = +∞)
Theorem	esumpcvgval 31946*	The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    &   ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Theorem	esumpmono 31947*	The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ (1...𝑀)𝐴 ≤ Σ*𝑘 ∈ (1...𝑁)𝐴)
Theorem	esumcocn 31948*	Lemma for esummulc2 31950 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐽 Cn 𝐽))    &   ⊢ (𝜑 → (𝐶‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) → (𝐶‘(𝑥 +𝑒 𝑦)) = ((𝐶‘𝑥) +𝑒 (𝐶‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐶‘Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶‘𝐵))
Theorem	esummulc1 31949*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶))
Theorem	esummulc2 31950*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (𝐶 ·e Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶 ·e 𝐵))
Theorem	esumdivc 31951*	An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 /𝑒 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 /𝑒 𝐶))
Theorem	hashf2 31952	Lemma for hasheuni 31953. (Contributed by Thierry Arnoux, 19-Nov-2016.)
⊢ ♯:V⟶(0[,]+∞)
Theorem	hasheuni 31953*	The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15466. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (♯‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(♯‘𝑥))
Theorem	esumcvg 31954*	The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 15367. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvg2 31955*	Simpler version of esumcvg 31954. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvgsum 31956*	The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.)
⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Theorem	esumsup 31957*	Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴), ℝ*, < ))
Theorem	esumgect 31958*	"Send 𝑛 to +∞ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 ≤ 𝐵)
Theorem	esumcvgre 31959*	All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
Theorem	esum2dlem 31960*	Lemma for esum2d 31961 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
Theorem	esum2d 31961*	Write a double extended sum as a sum over a two-dimensional region. Note that 𝐵(𝑗) is a function of 𝑗. This can be seen as "slicing" the relation 𝐴. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
Theorem	esumiun 31962*	Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)
20.3.16  Mixed Function/Constant operation
Syntax	cofc 31963	Extend class notation to include mapping of an operation to an operation for a function and a constant.
class ∘f/c 𝑅
Definition	df-ofc 31964*	Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘f/c 𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ∘f/c 𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)))
Theorem	ofceq 31965	Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆)
Theorem	ofcfval 31966*	Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcval 31967	Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f/c 𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶))
Theorem	ofcfn 31968	The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) Fn 𝐴)
Theorem	ofcfeqd2 31969*	Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶))    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f/c 𝑃𝐶))
Theorem	ofcfval3 31970*	General value of (𝐹 ∘f/c 𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶)))
Theorem	ofcf 31971*	The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶):𝐴⟶𝑈)
Theorem	ofcfval2 31972*	The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcfval4 31973*	The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹))
Theorem	ofcc 31974	Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f/c 𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)}))
Theorem	ofcof 31975	Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f 𝑅(𝐴 × {𝐶})))
20.3.17  Abstract measure
20.3.17.1  Sigma-Algebra
Syntax	csiga 31976	Extend class notation to include the function giving the sigma-algebras on a given base set.
class sigAlgebra
Definition	df-siga 31977*	Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using 𝑆 and 𝑂 as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.)
⊢ sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})
Theorem	sigaex 31978*	Lemma for issiga 31980 and isrnsiga 31981. The class of sigma-algebras with base set 𝑜 is a set. Note: a more generic version with (𝑂 ∈ V → ...) could be useful for sigaval 31979. (Contributed by Thierry Arnoux, 24-Oct-2016.)
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))} ∈ V
Theorem	sigaval 31979*	The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.)
⊢ (𝑂 ∈ V → (sigAlgebra‘𝑂) = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})
Theorem	issiga 31980*	An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.)
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))))
Theorem	isrnsiga 31981*	The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (Proof shortened by Thierry Arnoux, 23-Oct-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))))
Theorem	0elsiga 31982	A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆)
Theorem	baselsiga 31983	A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆)
Theorem	sigasspw 31984	A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴)
Theorem	sigaclcu 31985	A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcuni 31986*	A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	sigaclfu 31987	A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcu2 31988*	A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆)
Theorem	sigaclfu2 31989*	A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆)
Theorem	sigaclcu3 31990*	A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆)
Theorem	issgon 31991	Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016.) (Revised by Thierry Arnoux, 23-Oct-2016.)
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆))
Theorem	sgon 31992	A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
Theorem	elsigass 31993	An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆)
Theorem	elrnsiga 31994	Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	isrnsigau 31995*	The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))
Theorem	unielsiga 31996	A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017.) (Shortened by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
Theorem	dmvlsiga 31997	Lebesgue-measurable subsets of ℝ form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
⊢ dom vol ∈ (sigAlgebra‘ℝ)
Theorem	pwsiga 31998	Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂))
Theorem	prsiga 31999	The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.)
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂))
Theorem	sigaclci 32000	A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.)
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆)