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	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ 𝐴 ) ) = ( 1 − ( 𝑃 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → 𝑃 ∈ Prob )
2	1	unveldomd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ∪ dom 𝑃 ∈ dom 𝑃 )
3		simpr	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → 𝐴 ∈ dom 𝑃 )
4		probdif	⊢ ( ( 𝑃 ∈ Prob ∧ ∪ dom 𝑃 ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ 𝐴 ) ) = ( ( 𝑃 ‘ ∪ dom 𝑃 ) − ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ 𝐴 ) ) = ( ( 𝑃 ‘ ∪ dom 𝑃 ) − ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) ) )
6		probtot	⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 )
7		elssuni	⊢ ( 𝐴 ∈ dom 𝑃 → 𝐴 ⊆ ∪ dom 𝑃 )
8		sseqin2	⊢ ( 𝐴 ⊆ ∪ dom 𝑃 ↔ ( ∪ dom 𝑃 ∩ 𝐴 ) = 𝐴 )
9	7 8	sylib	⊢ ( 𝐴 ∈ dom 𝑃 → ( ∪ dom 𝑃 ∩ 𝐴 ) = 𝐴 )
10	9	fveq2d	⊢ ( 𝐴 ∈ dom 𝑃 → ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) = ( 𝑃 ‘ 𝐴 ) )
11	6 10	oveqan12d	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( ( 𝑃 ‘ ∪ dom 𝑃 ) − ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) ) = ( 1 − ( 𝑃 ‘ 𝐴 ) ) )
12	5 11	eqtrd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ 𝐴 ) ) = ( 1 − ( 𝑃 ‘ 𝐴 ) ) )