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 𝑃 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑃 ‘ 𝐴 ) ≤ ( 𝑃 ‘ 𝐵 ) ) |