Theorem probcun

Description: The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the sum_ construct cannot be used as it can handle infinite indexing set only if they are subsets of ZZ , which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016)

	Ref	Expression
Assertion	probcun	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑃 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑃 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
2		measvun	⊢ ( ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑃 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑃 ‘ 𝑥 ) )
3	1 2	syl3an1	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑃 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑃 ‘ 𝑥 ) )