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 \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to P (A) \leq P (B)$

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to P \in Prob$
2		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
3	1 2	syl	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to P \in measures (dom P)$
4		simpl2	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to A \in dom P$
5		simpl3	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to B \in dom P$
6		simpr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to A \subseteq B$
7	3 4 5 6	measssd	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \subseteq B) \to P (A) \leq P (B)$

Metamath Proof Explorer