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 = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccprob	|- cprob
1		vp	|- p
2		cprb	|- Prob
3		va	|- a
4	1	cv	|- p
5	4	cdm	|- dom p
6		vb	|- b
7	3	cv	|- a
8	6	cv	|- b
9	7 8	cin	|- ( a i^i b )
10	9 4	cfv	|- ( p ` ( a i^i b ) )
11		cdiv	|- /
12	8 4	cfv	|- ( p ` b )
13	10 12 11	co	|- ( ( p ` ( a i^i b ) ) / ( p ` b ) )
14	3 6 5 5 13	cmpo	|- ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) )
15	1 2 14	cmpt	|- ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )
16	0 15	wceq	|- cprob = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )