Metamath Proof Explorer

Theorem probdsb

Description: The probability of the complement of a set. That is, the probability that the event A does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016)

		Ref	Expression
	Assertion	probdsb	$⊢ (P \in Prob \land A \in dom P) \to P (⋃ dom P ∖ A) = 1 - P (A)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (P \in Prob \land A \in dom P) \to P \in Prob$
2	1	unveldomd	$⊢ (P \in Prob \land A \in dom P) \to ⋃ dom P \in dom P$
3		simpr	$⊢ (P \in Prob \land A \in dom P) \to A \in dom P$
4		probdif	$⊢ (P \in Prob \land ⋃ dom P \in dom P \land A \in dom P) \to P (⋃ dom P ∖ A) = P (⋃ dom P) - P (⋃ dom P \cap A)$
5	1 2 3 4	syl3anc	$⊢ (P \in Prob \land A \in dom P) \to P (⋃ dom P ∖ A) = P (⋃ dom P) - P (⋃ dom P \cap A)$
6		probtot	$⊢ P \in Prob \to P (⋃ dom P) = 1$
7		elssuni	$⊢ A \in dom P \to A \subseteq ⋃ dom P$
8		sseqin2	$⊢ A \subseteq ⋃ dom P \leftrightarrow ⋃ dom P \cap A = A$
9	7 8	sylib	$⊢ A \in dom P \to ⋃ dom P \cap A = A$
10	9	fveq2d	$⊢ A \in dom P \to P (⋃ dom P \cap A) = P (A)$
11	6 10	oveqan12d	$⊢ (P \in Prob \land A \in dom P) \to P (⋃ dom P) - P (⋃ dom P \cap A) = 1 - P (A)$
12	5 11	eqtrd	$⊢ (P \in Prob \land A \in dom P) \to P (⋃ dom P ∖ A) = 1 - P (A)$