| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ov 7435 | . 2
⊢ (𝐴(cprob‘𝑃)𝐵) = ((cprob‘𝑃)‘〈𝐴, 𝐵〉) | 
| 2 |  | df-cndprob 34435 | . . . . 5
⊢ cprob =
(𝑝 ∈ Prob ↦
(𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))) | 
| 3 |  | dmeq 5913 | . . . . . 6
⊢ (𝑝 = 𝑃 → dom 𝑝 = dom 𝑃) | 
| 4 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝‘(𝑎 ∩ 𝑏)) = (𝑃‘(𝑎 ∩ 𝑏))) | 
| 5 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝‘𝑏) = (𝑃‘𝑏)) | 
| 6 | 4, 5 | oveq12d 7450 | . . . . . 6
⊢ (𝑝 = 𝑃 → ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)) = ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) | 
| 7 | 3, 3, 6 | mpoeq123dv 7509 | . . . . 5
⊢ (𝑝 = 𝑃 → (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) | 
| 8 |  | id 22 | . . . . 5
⊢ (𝑃 ∈ Prob → 𝑃 ∈ Prob) | 
| 9 |  | dmexg 7924 | . . . . . 6
⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ V) | 
| 10 |  | mpoexga 8103 | . . . . . 6
⊢ ((dom
𝑃 ∈ V ∧ dom 𝑃 ∈ V) → (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) ∈ V) | 
| 11 | 9, 9, 10 | syl2anc 584 | . . . . 5
⊢ (𝑃 ∈ Prob → (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏))) ∈ V) | 
| 12 | 2, 7, 8, 11 | fvmptd3 7038 | . . . 4
⊢ (𝑃 ∈ Prob →
(cprob‘𝑃) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) | 
| 13 | 12 | 3ad2ant1 1133 | . . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (cprob‘𝑃) = (𝑎 ∈ dom 𝑃, 𝑏 ∈ dom 𝑃 ↦ ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)))) | 
| 14 |  | simprl 770 | . . . . . 6
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → 𝑎 = 𝐴) | 
| 15 |  | simprr 772 | . . . . . 6
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → 𝑏 = 𝐵) | 
| 16 | 14, 15 | ineq12d 4220 | . . . . 5
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑎 ∩ 𝑏) = (𝐴 ∩ 𝐵)) | 
| 17 | 16 | fveq2d 6909 | . . . 4
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑃‘(𝑎 ∩ 𝑏)) = (𝑃‘(𝐴 ∩ 𝐵))) | 
| 18 | 15 | fveq2d 6909 | . . . 4
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑃‘𝑏) = (𝑃‘𝐵)) | 
| 19 | 17, 18 | oveq12d 7450 | . . 3
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → ((𝑃‘(𝑎 ∩ 𝑏)) / (𝑃‘𝑏)) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) | 
| 20 |  | simp2 1137 | . . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → 𝐴 ∈ dom 𝑃) | 
| 21 |  | simp3 1138 | . . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → 𝐵 ∈ dom 𝑃) | 
| 22 |  | ovexd 7467 | . . 3
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵)) ∈ V) | 
| 23 | 13, 19, 20, 21, 22 | ovmpod 7586 | . 2
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝐴(cprob‘𝑃)𝐵) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) | 
| 24 | 1, 23 | eqtr3id 2790 | 1
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) |