P. 347 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34601-34700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	esumdivc 34601*	An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 /𝑒 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 /𝑒 𝐶))
Theorem	hashf2 34602	Lemma for hasheuni 34603. (Contributed by Thierry Arnoux, 19-Nov-2016.)
⊢ ♯:V⟶(0[,]+∞)
Theorem	hasheuni 34603*	The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15917. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (♯‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(♯‘𝑥))
Theorem	esumcvg 34604*	The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 15817. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvg2 34605*	Simpler version of esumcvg 34604. (Contributed by Thierry Arnoux, 5-Sep-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴)
Theorem	esumcvgsum 34606*	The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.)
⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Theorem	esumsup 34607*	Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴), ℝ*, < ))
Theorem	esumgect 34608*	"Send 𝑛 to +∞ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 ≤ 𝐵)
Theorem	esumcvgre 34609*	All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
Theorem	esum2dlem 34610*	Lemma for esum2d 34611 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
Theorem	esum2d 34611*	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 34612*	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[,]+∞))    ⇒   ⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)
21.3.17  Mixed Function/Constant operation
Syntax	cofc 34613	Extend class notation to include mapping of an operation to an operation for a function and a constant.
class ∘f/c 𝑅
Definition	df-ofc 34614*	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 34615	Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆)
Theorem	ofcfval 34616*	Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcval 34617	Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f/c 𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶))
Theorem	ofcfn 34618	The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) Fn 𝐴)
Theorem	ofcfeqd2 34619*	Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶))    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f/c 𝑃𝐶))
Theorem	ofcfval3 34620*	General value of (𝐹 ∘f/c 𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶)))
Theorem	ofcf 34621*	The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶):𝐴⟶𝑈)
Theorem	ofcfval2 34622*	The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofcfval4 34623*	The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹))
Theorem	ofcc 34624	Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f/c 𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)}))
Theorem	ofcof 34625	Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f 𝑅(𝐴 × {𝐶})))
21.3.18  Abstract measure
21.3.18.1  Sigma-Algebra
Syntax	csiga 34626	Extend class notation to include the function giving the sigma-algebras on a given base set.
class sigAlgebra
Definition	df-siga 34627*	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 34628*	Lemma for issiga 34630 and isrnsiga 34631. The class of sigma-algebras with base set 𝑜 is a set. Note: a more generic version with (𝑂 ∈ V → ...) could be useful for sigaval 34629. (Contributed by Thierry Arnoux, 24-Oct-2016.)
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))} ∈ V
Theorem	sigaval 34629*	The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.)
⊢ (𝑂 ∈ V → (sigAlgebra‘𝑂) = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})
Theorem	issiga 34630*	An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.)
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))))
Theorem	isrnsiga 34631*	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 34632	A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆)
Theorem	baselsiga 34633	A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆)
Theorem	sigasspw 34634	A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴)
Theorem	sigaclcu 34635	A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcuni 34636*	A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	sigaclfu 34637	A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcu2 34638*	A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆)
Theorem	sigaclfu2 34639*	A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆)
Theorem	sigaclcu3 34640*	A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆)
Theorem	issgon 34641	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 34642	A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
Theorem	elsigass 34643	An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆)
Theorem	elrnsiga 34644	Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	isrnsigau 34645*	The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))
Theorem	unielsiga 34646	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 34647	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 34648	Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂))
Theorem	prsiga 34649	The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.)
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂))
Theorem	sigaclci 34650	A sigma-algebra is closed under countable intersections. Deduction version. The proof uses abrexct 23686 rather than abrexdom2jm 32991, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 19-Sep-2016.) (Revised by Vincent Gonzalez, 19-Aug-2026.)
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆)
Theorem	difunielsiga 34651	A sigma-algebra is closed under complement relative to its base set. This is immediate from the definition, see issiga 34630, but the library states it nowhere in this form. (Contributed by Vincent Gonzalez, 17-Aug-2026.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐴) ∈ 𝑆)
Theorem	unelsiga 34652	A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	difelsiga 34653	A sigma-algebra is closed under class differences. The proof goes through difunielsiga 34651 and unelsiga 34652 rather than countable intersection, and so does not use ax-ac 10465. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Proof shortened by Vincent Gonzalez, 17-Aug-2026.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelsiga 34654	A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigainb 34655	Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴))
Theorem	insiga 34656	The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
21.3.18.2  Generated sigma-Algebra
Syntax	csigagen 34657	Extend class notation to include the sigma-algebra generator.
class sigaGen
Definition	df-sigagen 34658*	Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})
Theorem	sigagenval 34659*	Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠})
Theorem	sigagensiga 34660	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) ∈ (sigAlgebra‘∪ 𝐴))
Theorem	sgsiga 34661	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (sigaGen‘𝐴) ∈ ∪ ran sigAlgebra)
Theorem	unisg 34662	The sigma-algebra generated by a collection 𝐴 is a sigma-algebra on ∪ 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → ∪ (sigaGen‘𝐴) = ∪ 𝐴)
Theorem	dmsigagen 34663	A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ dom sigaGen = V
Theorem	sssigagen 34664	A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (sigaGen‘𝐴))
Theorem	sssigagen2 34665	A subset of the generating set is also a subset of the generated sigma-algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ (sigaGen‘𝐴))
Theorem	elsigagen 34666	Any element of a set is also an element of the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 27-Mar-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ (sigaGen‘𝐴))
Theorem	elsigagen2 34667	Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω) → ∪ 𝐵 ∈ (sigaGen‘𝐴))
Theorem	sigagenss 34668	The generated sigma-algebra is a subset of all sigma-algebras containing the generating set, i.e. the generated sigma-algebra is the smallest sigma-algebra containing the generating set, here 𝐴. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ ((𝑆 ∈ (sigAlgebra‘∪ 𝐴) ∧ 𝐴 ⊆ 𝑆) → (sigaGen‘𝐴) ⊆ 𝑆)
Theorem	sigagenss2 34669	Sufficient condition for inclusion of sigma-algebras. This is used to prove equality of sigma-algebras. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ ((∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ (sigaGen‘𝐵) ∧ 𝐵 ∈ 𝑉) → (sigaGen‘𝐴) ⊆ (sigaGen‘𝐵))
Theorem	sigagenid 34670	The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (sigaGen‘𝑆) = 𝑆)
21.3.18.3  lambda and pi-Systems, Rings of Sets Because they are not widely used outside of measure theory, we do not introduce specific definitions for lambda- and pi-systems. Instead, we define 𝑃 and 𝐿 respectively as the classes of pi- and lambda-systems in 𝑂 throughout this section.
Theorem	ispisys 34671*	The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑆) ⊆ 𝑆))
Theorem	ispisys2 34672*	The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀𝑥 ∈ ((𝒫 𝑆 ∩ Fin) ∖ {∅})∩ 𝑥 ∈ 𝑆))
Theorem	inelpisys 34673*	Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ ((𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigapisys 34674*	All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝑃
Theorem	isldsys 34675*	The property of being a lambda-system or Dynkin system. Lambda-systems contain the empty set, are closed under complement, and closed under countable disjoint union. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆))))
Theorem	pwldsys 34676*	The power set of the universe set 𝑂 is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿)
Theorem	unelldsys 34677*	Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	sigaldsys 34678*	All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝐿
Theorem	ldsysgenld 34679*	The intersection of all lambda-systems containing a given collection of sets 𝐴, which is called the lambda-system generated by 𝐴, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑂)    ⇒   ⊢ (𝜑 → ∩ {𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡} ∈ 𝐿)
Theorem	sigapildsyslem 34680*	Lemma for sigapildsys 34681. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑡)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡)    ⇒   ⊢ (𝜑 → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) ∈ 𝑡)
Theorem	sigapildsys 34681*	Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) = (𝑃 ∩ 𝐿)
Theorem	ldgenpisyslem1 34682*	Lemma for ldgenpisys 34685. (Contributed by Thierry Arnoux, 29-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿)
Theorem	ldgenpisyslem2 34683*	Lemma for ldgenpisys 34685. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑇 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisyslem3 34684*	Lemma for ldgenpisys 34685. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisys 34685*	The lambda system 𝐸 generated by a pi-system 𝑇 is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑃)
Theorem	dynkin 34686*	Dynkin's lambda-pi theorem: if a lambda-system contains a pi-system, it also contains the sigma-algebra generated by that pi-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ∩ {𝑢 ∈ (sigAlgebra‘𝑂) ∣ 𝑇 ⊆ 𝑢} ⊆ 𝑆)
Theorem	isros 34687*	The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ (𝑢 ∖ 𝑣) ∈ 𝑆)))
Theorem	rossspw 34688*	A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elros 34689*	A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆)
Theorem	unelros 34690*	A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	difelros 34691*	A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelros 34692*	A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	fiunelros 34693*	A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)
Theorem	issros 34694*	The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧))))
Theorem	srossspw 34695*	A semiring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elsros 34696*	A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆)
Theorem	inelsros 34697*	A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	diffiunisros 34698*	In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))
Theorem	rossros 34699*	Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁)
21.3.18.4  The Borel algebra on the real numbers
Syntax	cbrsiga 34700	The Borel Algebra on real numbers, usually a gothic B
class 𝔅ℝ