P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0elsiga 33601	A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆)
Theorem	baselsiga 33602	A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆)
Theorem	sigasspw 33603	A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴)
Theorem	sigaclcu 33604	A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcuni 33605*	A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	sigaclfu 33606	A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆)
Theorem	sigaclcu2 33607*	A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆)
Theorem	sigaclfu2 33608*	A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆)
Theorem	sigaclcu3 33609*	A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆)
Theorem	issgon 33610	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 33611	A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
Theorem	elsigass 33612	An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆)
Theorem	elrnsiga 33613	Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	isrnsigau 33614*	The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))
Theorem	unielsiga 33615	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 33616	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 33617	Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂))
Theorem	prsiga 33618	The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.)
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂))
Theorem	sigaclci 33619	A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.)
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆)
Theorem	difelsiga 33620	A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	unelsiga 33621	A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	inelsiga 33622	A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigainb 33623	Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴))
Theorem	insiga 33624	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.17.2  Generated sigma-Algebra
Syntax	csigagen 33625	Extend class notation to include the sigma-algebra generator.
class sigaGen
Definition	df-sigagen 33626*	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 33627*	Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠})
Theorem	sigagensiga 33628	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) ∈ (sigAlgebra‘∪ 𝐴))
Theorem	sgsiga 33629	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (sigaGen‘𝐴) ∈ ∪ ran sigAlgebra)
Theorem	unisg 33630	The sigma-algebra generated by a collection 𝐴 is a sigma-algebra on ∪ 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → ∪ (sigaGen‘𝐴) = ∪ 𝐴)
Theorem	dmsigagen 33631	A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ dom sigaGen = V
Theorem	sssigagen 33632	A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (sigaGen‘𝐴))
Theorem	sssigagen2 33633	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 33634	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 33635	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 33636	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 33637	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 33638	The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (sigaGen‘𝑆) = 𝑆)
21.3.17.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 33639*	The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑆) ⊆ 𝑆))
Theorem	ispisys2 33640*	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 33641*	Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ ((𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigapisys 33642*	All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝑃
Theorem	isldsys 33643*	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 33644*	The power set of the universe set 𝑂 is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿)
Theorem	unelldsys 33645*	Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	sigaldsys 33646*	All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝐿
Theorem	ldsysgenld 33647*	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 33648*	Lemma for sigapildsys 33649. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑡)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡)    ⇒   ⊢ (𝜑 → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) ∈ 𝑡)
Theorem	sigapildsys 33649*	Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) = (𝑃 ∩ 𝐿)
Theorem	ldgenpisyslem1 33650*	Lemma for ldgenpisys 33653. (Contributed by Thierry Arnoux, 29-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿)
Theorem	ldgenpisyslem2 33651*	Lemma for ldgenpisys 33653. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑇 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisyslem3 33652*	Lemma for ldgenpisys 33653. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisys 33653*	The lambda system 𝐸 generated by a pi-system 𝑇 is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑃)
Theorem	dynkin 33654*	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 33655*	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 33656*	A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elros 33657*	A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆)
Theorem	unelros 33658*	A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	difelros 33659*	A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelros 33660*	A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	fiunelros 33661*	A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)
Theorem	issros 33662*	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 33663*	A semiring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elsros 33664*	A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆)
Theorem	inelsros 33665*	A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	diffiunisros 33666*	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 33667*	Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁)
21.3.17.4  The Borel algebra on the real numbers
Syntax	cbrsiga 33668	The Borel Algebra on real numbers, usually a gothic B
class 𝔅ℝ
Definition	df-brsiga 33669	A Borel Algebra is defined as a sigma-algebra generated by a topology. 'The' Borel sigma-algebra here refers to the sigma-algebra generated by the topology of open intervals on real numbers. The Borel algebra of a given topology 𝐽 is the sigma-algebra generated by 𝐽, (sigaGen‘𝐽), so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ = (sigaGen‘(topGen‘ran (,)))
Theorem	brsiga 33670	The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigaGen “ Top)
Theorem	brsigarn 33671	The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigAlgebra‘ℝ)
Theorem	brsigasspwrn 33672	The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ 𝔅ℝ ⊆ 𝒫 ℝ
Theorem	unibrsiga 33673	The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ∪ 𝔅ℝ = ℝ
Theorem	cldssbrsiga 33674	A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.)
⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
21.3.17.5  Product Sigma-Algebra
Syntax	csx 33675	Extend class notation with the product sigma-algebra operation.
class ×s
Definition	df-sx 33676*	Define the product sigma-algebra operation, analogous to df-tx 23388. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))))
Theorem	sxval 33677*	Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ 𝐴 = ran (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑇 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ×s 𝑇) = (sigaGen‘𝐴))
Theorem	sxsiga 33678	A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra)
Theorem	sxsigon 33679	A product sigma-algebra is a sigma-algebra on the product of the bases. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ (sigAlgebra‘(∪ 𝑆 × ∪ 𝑇)))
Theorem	sxuni 33680	The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇))
Theorem	elsx 33681	The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐴 × 𝐵) ∈ (𝑆 ×s 𝑇))
21.3.17.6  Measures
Syntax	cmeas 33682	Extend class notation to include the class of measures.
class measures
Definition	df-meas 33683*	Define a measure as a nonnegative countably additive function over a sigma-algebra onto (0[,]+∞). (Contributed by Thierry Arnoux, 10-Sep-2016.)
⊢ measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
Theorem	measbase 33684	The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	measval 33685*	The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (measures‘𝑆) = {𝑚 ∣ (𝑚:𝑆⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
Theorem	ismeas 33686*	The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 19-Oct-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))))
Theorem	isrnmeas 33687*	The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures → (dom 𝑀 ∈ ∪ ran sigAlgebra ∧ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))))
Theorem	dmmeas 33688	The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
Theorem	measbasedom 33689	The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀))
Theorem	measfrge0 33690	A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
Theorem	measfn 33691	A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 Fn 𝑆)
Theorem	measvxrge0 33692	The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	measvnul 33693	The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
Theorem	measge0 33694	A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝑀‘𝐴))
Theorem	measle0 33695	If the measure of a given set is bounded by zero, it is zero. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ≤ 0) → (𝑀‘𝐴) = 0)
Theorem	measvun 33696*	The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑀‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑀‘𝑥))
Theorem	measxun2 33697	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵))))
Theorem	measun 33698	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measvunilem 33699*	Lemma for measvuni 33701. (Contributed by Thierry Arnoux, 7-Feb-2017.) (Revised by Thierry Arnoux, 19-Feb-2017.) (Revised by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvunilem0 33700*	Lemma for measvuni 33701. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ {∅} ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))