Step | Hyp | Ref
| Expression |
1 | | df-ov 6552 |
. 2
⊢ (𝐴(cprob‘𝑃)𝐵) = ((cprob‘𝑃)‘〈𝐴, 𝐵〉) |
2 | | df-cndprob 29821 |
. . . . . 6
⊢ cprob =
(𝑝 ∈ Prob ↦
(𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))) |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑃 ∈ Prob → cprob =
(𝑝 ∈ Prob ↦
(𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))) |
4 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → dom 𝑝 = dom 𝑃) |
5 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘(𝑎 ∩ 𝑏)) = (𝑃‘(𝑎 ∩ 𝑏))) |
6 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘𝑏) = (𝑃‘𝑏)) |
7 | 5, 6 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)) = ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) |
8 | 4, 4, 7 | mpt2eq123dv 6615 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) |
9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝑃 ∈ Prob ∧ 𝑝 = 𝑃) → (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) |
10 | | id 22 |
. . . . 5
⊢ (𝑃 ∈ Prob → 𝑃 ∈ Prob) |
11 | | dmexg 6989 |
. . . . . 6
⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ V) |
12 | | mpt2exga 7135 |
. . . . . 6
⊢ ((dom
𝑃 ∈ V ∧ dom 𝑃 ∈ V) → (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) ∈ V) |
13 | 11, 11, 12 | syl2anc 691 |
. . . . 5
⊢ (𝑃 ∈ Prob → (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) ∈ V) |
14 | 3, 9, 10, 13 | fvmptd 6197 |
. . . 4
⊢ (𝑃 ∈ Prob →
(cprob‘𝑃) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) |
15 | 14 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (cprob‘𝑃) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) |
16 | | simprl 790 |
. . . . . 6
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → 𝑎 = 𝐴) |
17 | | simprr 792 |
. . . . . 6
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → 𝑏 = 𝐵) |
18 | 16, 17 | ineq12d 3777 |
. . . . 5
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑎 ∩ 𝑏) = (𝐴 ∩ 𝐵)) |
19 | 18 | fveq2d 6107 |
. . . 4
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑃‘(𝑎 ∩ 𝑏)) = (𝑃‘(𝐴 ∩ 𝐵))) |
20 | 17 | fveq2d 6107 |
. . . 4
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑃‘𝑏) = (𝑃‘𝐵)) |
21 | 19, 20 | oveq12d 6567 |
. . 3
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) |
22 | | simp2 1055 |
. . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → 𝐴 ∈ dom 𝑃) |
23 | | simp3 1056 |
. . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → 𝐵 ∈ dom 𝑃) |
24 | | ovex 6577 |
. . . 4
⊢ ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵)) ∈ V |
25 | 24 | a1i 11 |
. . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵)) ∈ V) |
26 | 15, 21, 22, 23, 25 | ovmpt2d 6686 |
. 2
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝐴(cprob‘𝑃)𝐵) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) |
27 | 1, 26 | syl5eqr 2658 |
1
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) |