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 e. Prob /\ A e. ~P dom P /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( P ` U. A ) = sum* x e. A ( P ` x ) )

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	|- ( P e. Prob -> P e. ( measures ` dom P ) )
2		measvun	|- ( ( P e. ( measures ` dom P ) /\ A e. ~P dom P /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( P ` U. A ) = sum* x e. A ( P ` x ) )
3	1 2	syl3an1	|- ( ( P e. Prob /\ A e. ~P dom P /\ ( A ~<_ _om /\ Disj_ x e. A x ) ) -> ( P ` U. A ) = sum* x e. A ( P ` x ) )