Theorem probinc

Description: A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017)

	Ref	Expression
Assertion	probinc	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> ( P ` A ) <_ ( P ` B ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> P e. Prob )
2		domprobmeas	|- ( P e. Prob -> P e. ( measures ` dom P ) )
3	1 2	syl	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> P e. ( measures ` dom P ) )
4		simpl2	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> A e. dom P )
5		simpl3	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> B e. dom P )
6		simpr	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> A C_ B )
7	3 4 5 6	measssd	|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> ( P ` A ) <_ ( P ` B ) )