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 e. Prob /\ A e. dom P ) -> ( P ` ( U. dom P \ A ) ) = ( 1 - ( P ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( P e. Prob /\ A e. dom P ) -> P e. Prob )
2	1	unveldomd	|- ( ( P e. Prob /\ A e. dom P ) -> U. dom P e. dom P )
3		simpr	|- ( ( P e. Prob /\ A e. dom P ) -> A e. dom P )
4		probdif	|- ( ( P e. Prob /\ U. dom P e. dom P /\ A e. dom P ) -> ( P ` ( U. dom P \ A ) ) = ( ( P ` U. dom P ) - ( P ` ( U. dom P i^i A ) ) ) )
5	1 2 3 4	syl3anc	|- ( ( P e. Prob /\ A e. dom P ) -> ( P ` ( U. dom P \ A ) ) = ( ( P ` U. dom P ) - ( P ` ( U. dom P i^i A ) ) ) )
6		probtot	|- ( P e. Prob -> ( P ` U. dom P ) = 1 )
7		elssuni	|- ( A e. dom P -> A C_ U. dom P )
8		sseqin2	|- ( A C_ U. dom P <-> ( U. dom P i^i A ) = A )
9	7 8	sylib	|- ( A e. dom P -> ( U. dom P i^i A ) = A )
10	9	fveq2d	|- ( A e. dom P -> ( P ` ( U. dom P i^i A ) ) = ( P ` A ) )
11	6 10	oveqan12d	|- ( ( P e. Prob /\ A e. dom P ) -> ( ( P ` U. dom P ) - ( P ` ( U. dom P i^i A ) ) ) = ( 1 - ( P ` A ) ) )
12	5 11	eqtrd	|- ( ( P e. Prob /\ A e. dom P ) -> ( P ` ( U. dom P \ A ) ) = ( 1 - ( P ` A ) ) )