Metamath Proof Explorer


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 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → ( 𝑃𝐴 ) ≤ ( 𝑃𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl1 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → 𝑃 ∈ Prob )
2 domprobmeas ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
3 1 2 syl ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
4 simpl2 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → 𝐴 ∈ dom 𝑃 )
5 simpl3 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → 𝐵 ∈ dom 𝑃 )
6 simpr ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → 𝐴𝐵 )
7 3 4 5 6 measssd ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃 ) ∧ 𝐴𝐵 ) → ( 𝑃𝐴 ) ≤ ( 𝑃𝐵 ) )