Definition df-cndprob

Description: Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Assertion	df-cndprob	⊢ cprob = ( 𝑝 ∈ Prob ↦ ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccprob	⊢ cprob
1		vp	⊢ 𝑝
2		cprb	⊢ Prob
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑝
5	4	cdm	⊢ dom 𝑝
6		vb	⊢ 𝑏
7	3	cv	⊢ 𝑎
8	6	cv	⊢ 𝑏
9	7 8	cin	⊢ ( 𝑎 ∩ 𝑏 )
10	9 4	cfv	⊢ ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) )
11		cdiv	⊢ /
12	8 4	cfv	⊢ ( 𝑝 ‘ 𝑏 )
13	10 12 11	co	⊢ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) )
14	3 6 5 5 13	cmpo	⊢ ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑝 ∈ Prob ↦ ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) ) )
16	0 15	wceq	⊢ cprob = ( 𝑝 ∈ Prob ↦ ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) ) )