Metamath Proof Explorer

Theorem probun

Description: The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion probun ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpll1 ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 = 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑃 ∈ Prob )
2 simplr ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 = 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 = 𝐵 )
3 simpr ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 = 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
4 disj3 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ 𝐵 ) )
5 4 biimpi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → 𝐴 = ( 𝐴 ∖ 𝐵 ) )
6 difeq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∖ 𝐵 ) = ( 𝐵 ∖ 𝐵 ) )
7 difid ⊢ ( 𝐵 ∖ 𝐵 ) = ∅
8 6 7 eqtrdi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∖ 𝐵 ) = ∅ )
9 5 8 sylan9eqr ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 = ∅ )
10 eqtr2 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 = ∅ ) → 𝐵 = ∅ )
11 9 10 syldan ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 = ∅ )
12 9 11 uneq12d ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) = ( ∅ ∪ ∅ ) )
13 unidm ⊢ ( ∅ ∪ ∅ ) = ∅
14 12 13 eqtrdi ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) = ∅ )
15 14 fveq2d ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑃 ‘ ∅ ) )
16 probnul ⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∅ ) = 0 )
17 15 16 sylan9eqr ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = 0 )
18 9 fveq2d ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ∅ ) )
19 18 16 sylan9eqr ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( 𝑃 ‘ 𝐴 ) = 0 )
20 11 fveq2d ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ∅ ) )
21 20 16 sylan9eqr ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( 𝑃 ‘ 𝐵 ) = 0 )
22 19 21 oveq12d ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) = ( 0 + 0 ) )
23 00id ⊢ ( 0 + 0 ) = 0
24 22 23 eqtrdi ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) = 0 )
25 17 24 eqtr4d ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) )
26 1 2 3 25 syl12anc ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 = 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) )
27 26 ex ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 = 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) ) )
28 3anass ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ↔ ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ) )
29 28 anbi1i ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ) ∧ 𝐴 ≠ 𝐵 ) )
30 df-3an ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ) ∧ 𝐴 ≠ 𝐵 ) )
31 29 30 bitr4i ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) )
32 simpl1 ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑃 ∈ Prob )
33 prssi ⊢ ( ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → { 𝐴 , 𝐵 } ⊆ dom 𝑃 )
34 33 3ad2ant2 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ⊆ dom 𝑃 )
35 34 adantr ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → { 𝐴 , 𝐵 } ⊆ dom 𝑃 )
36 prex ⊢ { 𝐴 , 𝐵 } ∈ V
37 36 elpw ⊢ ( { 𝐴 , 𝐵 } ∈ 𝒫 dom 𝑃 ↔ { 𝐴 , 𝐵 } ⊆ dom 𝑃 )
38 35 37 sylibr ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → { 𝐴 , 𝐵 } ∈ 𝒫 dom 𝑃 )
39 prct ⊢ ( ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → { 𝐴 , 𝐵 } ≼ ω )
40 39 3ad2ant2 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≼ ω )
41 40 adantr ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → { 𝐴 , 𝐵 } ≼ ω )
42 simp2l ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ dom 𝑃 )
43 simp2r ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ dom 𝑃 )
44 simp3 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
45 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
46 id ⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
47 45 46 disjprg ⊢ ( ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ∧ 𝐴 ≠ 𝐵 ) → ( Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
48 42 43 44 47 syl3anc ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
49 48 biimpar ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 )
50 probcun ⊢ ( ( 𝑃 ∈ Prob ∧ { 𝐴 , 𝐵 } ∈ 𝒫 dom 𝑃 ∧ ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = Σ* 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑃 ‘ 𝑥 ) )
51 32 38 41 49 50 syl112anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = Σ* 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑃 ‘ 𝑥 ) )
52 uniprg ⊢ ( ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
53 52 fveq2d ⊢ ( ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) )
54 53 3ad2ant2 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) )
55 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐴 ) )
56 55 adantl ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 = 𝐴 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐴 ) )
57 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐵 ) )
58 57 adantl ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 = 𝐵 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐵 ) )
59 unitssxrge0 ⊢ ( 0 [,] 1 ) ⊆ ( 0 [,] +∞ )
60 simp1 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑃 ∈ Prob )
61 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
62 60 42 61 syl2anc ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
63 59 62 sselid ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
64 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
65 60 43 64 syl2anc ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
66 59 65 sselid ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
67 56 58 42 43 63 66 44 esumpr ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → Σ* 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑃 ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) )
68 54 67 eqeq12d ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = Σ* 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) ) )
69 68 adantr ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑃 ‘ ∪ { 𝐴 , 𝐵 } ) = Σ* 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) ) )
70 51 69 mpbid ⊢ ( ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) )
71 31 70 sylanb ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) )
72 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
73 simpll1 ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑃 ∈ Prob )
74 simpll2 ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ dom 𝑃 )
75 73 74 61 syl2anc ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
76 72 75 sselid ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐴 ) ∈ ℝ )
77 simpll3 ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ dom 𝑃 )
78 73 77 64 syl2anc ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
79 72 78 sselid ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ 𝐵 ) ∈ ℝ )
80 rexadd ⊢ ( ( ( 𝑃 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑃 ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) )
81 76 79 80 syl2anc ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) )
82 71 81 eqtrd ⊢ ( ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) )
83 82 ex ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) ) )
84 27 83 pm2.61dane ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝑃 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) + ( 𝑃 ‘ 𝐵 ) ) ) )