Theorem cndprobtot

Description: The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Assertion	cndprobtot	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∪ dom 𝑃 , 𝐴 ⟩ ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → 𝑃 ∈ Prob )
2	1	unveldomd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ∪ dom 𝑃 ∈ dom 𝑃 )
3		simpr	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → 𝐴 ∈ dom 𝑃 )
4		cndprobval	⊢ ( ( 𝑃 ∈ Prob ∧ ∪ dom 𝑃 ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∪ dom 𝑃 , 𝐴 ⟩ ) = ( ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∪ dom 𝑃 , 𝐴 ⟩ ) = ( ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) )
6	5	3adant3	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∪ dom 𝑃 , 𝐴 ⟩ ) = ( ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) )
7		elssuni	⊢ ( 𝐴 ∈ dom 𝑃 → 𝐴 ⊆ ∪ dom 𝑃 )
8	7	3ad2ant2	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → 𝐴 ⊆ ∪ dom 𝑃 )
9		sseqin2	⊢ ( 𝐴 ⊆ ∪ dom 𝑃 ↔ ( ∪ dom 𝑃 ∩ 𝐴 ) = 𝐴 )
10	8 9	sylib	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ∪ dom 𝑃 ∩ 𝐴 ) = 𝐴 )
11	10	fveq2d	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) = ( 𝑃 ‘ 𝐴 ) )
12	11	oveq1d	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑃 ‘ ( ∪ dom 𝑃 ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) = ( ( 𝑃 ‘ 𝐴 ) / ( 𝑃 ‘ 𝐴 ) ) )
13		prob01	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
14	13	3adant3	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
15		elunitcn	⊢ ( ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) → ( 𝑃 ‘ 𝐴 ) ∈ ℂ )
16	14 15	syl	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ∈ ℂ )
17		simp3	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ≠ 0 )
18	16 17	dividd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑃 ‘ 𝐴 ) / ( 𝑃 ‘ 𝐴 ) ) = 1 )
19	6 12 18	3eqtrd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∪ dom 𝑃 , 𝐴 ⟩ ) = 1 )