Metamath Proof Explorer

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	$⊢ (P \in Prob \land A \in 𝒫 dom P \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to P (⋃ A) = \underset{x \in A}{\sum^{*}} P (x)$

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
2		measvun	$⊢ (P \in measures (dom P) \land A \in 𝒫 dom P \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to P (⋃ A) = \underset{x \in A}{\sum^{*}} P (x)$
3	1 2	syl3an1	$⊢ (P \in Prob \land A \in 𝒫 dom P \land (A ≼ ω \land \underset{x \in A}{Disj} x)) \to P (⋃ A) = \underset{x \in A}{\sum^{*}} P (x)$