Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  probun Structured version   Visualization version   GIF version

Theorem probun 33233
Description: The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Assertion
Ref Expression
probun ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → ((𝐴𝐵) = ∅ → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵))))

Proof of Theorem probun
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpll1 1212 . . . 4 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴 = 𝐵) ∧ (𝐴𝐵) = ∅) → 𝑃 ∈ Prob)
2 simplr 767 . . . 4 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴 = 𝐵) ∧ (𝐴𝐵) = ∅) → 𝐴 = 𝐵)
3 simpr 485 . . . 4 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴 = 𝐵) ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) = ∅)
4 disj3 4446 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
54biimpi 215 . . . . . . . . . 10 ((𝐴𝐵) = ∅ → 𝐴 = (𝐴𝐵))
6 difeq1 4108 . . . . . . . . . . 11 (𝐴 = 𝐵 → (𝐴𝐵) = (𝐵𝐵))
7 difid 4363 . . . . . . . . . . 11 (𝐵𝐵) = ∅
86, 7eqtrdi 2787 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴𝐵) = ∅)
95, 8sylan9eqr 2793 . . . . . . . . 9 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → 𝐴 = ∅)
10 eqtr2 2755 . . . . . . . . . 10 ((𝐴 = 𝐵𝐴 = ∅) → 𝐵 = ∅)
119, 10syldan 591 . . . . . . . . 9 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → 𝐵 = ∅)
129, 11uneq12d 4157 . . . . . . . 8 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) = (∅ ∪ ∅))
13 unidm 4145 . . . . . . . 8 (∅ ∪ ∅) = ∅
1412, 13eqtrdi 2787 . . . . . . 7 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) = ∅)
1514fveq2d 6879 . . . . . 6 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → (𝑃‘(𝐴𝐵)) = (𝑃‘∅))
16 probnul 33228 . . . . . 6 (𝑃 ∈ Prob → (𝑃‘∅) = 0)
1715, 16sylan9eqr 2793 . . . . 5 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → (𝑃‘(𝐴𝐵)) = 0)
189fveq2d 6879 . . . . . . . 8 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → (𝑃𝐴) = (𝑃‘∅))
1918, 16sylan9eqr 2793 . . . . . . 7 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → (𝑃𝐴) = 0)
2011fveq2d 6879 . . . . . . . 8 ((𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅) → (𝑃𝐵) = (𝑃‘∅))
2120, 16sylan9eqr 2793 . . . . . . 7 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → (𝑃𝐵) = 0)
2219, 21oveq12d 7408 . . . . . 6 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → ((𝑃𝐴) + (𝑃𝐵)) = (0 + 0))
23 00id 11368 . . . . . 6 (0 + 0) = 0
2422, 23eqtrdi 2787 . . . . 5 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → ((𝑃𝐴) + (𝑃𝐵)) = 0)
2517, 24eqtr4d 2774 . . . 4 ((𝑃 ∈ Prob ∧ (𝐴 = 𝐵 ∧ (𝐴𝐵) = ∅)) → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵)))
261, 2, 3, 25syl12anc 835 . . 3 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴 = 𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵)))
2726ex 413 . 2 (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴 = 𝐵) → ((𝐴𝐵) = ∅ → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵))))
28 3anass 1095 . . . . . . 7 ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ↔ (𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃)))
2928anbi1i 624 . . . . . 6 (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ↔ ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃)) ∧ 𝐴𝐵))
30 df-3an 1089 . . . . . 6 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ↔ ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃)) ∧ 𝐴𝐵))
3129, 30bitr4i 277 . . . . 5 (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ↔ (𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵))
32 simpl1 1191 . . . . . . 7 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → 𝑃 ∈ Prob)
33 prssi 4814 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → {𝐴, 𝐵} ⊆ dom 𝑃)
34333ad2ant2 1134 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → {𝐴, 𝐵} ⊆ dom 𝑃)
3534adantr 481 . . . . . . . 8 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → {𝐴, 𝐵} ⊆ dom 𝑃)
36 prex 5422 . . . . . . . . 9 {𝐴, 𝐵} ∈ V
3736elpw 4597 . . . . . . . 8 ({𝐴, 𝐵} ∈ 𝒫 dom 𝑃 ↔ {𝐴, 𝐵} ⊆ dom 𝑃)
3835, 37sylibr 233 . . . . . . 7 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → {𝐴, 𝐵} ∈ 𝒫 dom 𝑃)
39 prct 31805 . . . . . . . . 9 ((𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → {𝐴, 𝐵} ≼ ω)
40393ad2ant2 1134 . . . . . . . 8 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → {𝐴, 𝐵} ≼ ω)
4140adantr 481 . . . . . . 7 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → {𝐴, 𝐵} ≼ ω)
42 simp2l 1199 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → 𝐴 ∈ dom 𝑃)
43 simp2r 1200 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → 𝐵 ∈ dom 𝑃)
44 simp3 1138 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → 𝐴𝐵)
45 id 22 . . . . . . . . . 10 (𝑥 = 𝐴𝑥 = 𝐴)
46 id 22 . . . . . . . . . 10 (𝑥 = 𝐵𝑥 = 𝐵)
4745, 46disjprg 5134 . . . . . . . . 9 ((𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃𝐴𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝑥 ↔ (𝐴𝐵) = ∅))
4842, 43, 44, 47syl3anc 1371 . . . . . . . 8 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝑥 ↔ (𝐴𝐵) = ∅))
4948biimpar 478 . . . . . . 7 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥)
50 probcun 33232 . . . . . . 7 ((𝑃 ∈ Prob ∧ {𝐴, 𝐵} ∈ 𝒫 dom 𝑃 ∧ ({𝐴, 𝐵} ≼ ω ∧ Disj 𝑥 ∈ {𝐴, 𝐵}𝑥)) → (𝑃 {𝐴, 𝐵}) = Σ*𝑥 ∈ {𝐴, 𝐵} (𝑃𝑥))
5132, 38, 41, 49, 50syl112anc 1374 . . . . . 6 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃 {𝐴, 𝐵}) = Σ*𝑥 ∈ {𝐴, 𝐵} (𝑃𝑥))
52 uniprg 4915 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → {𝐴, 𝐵} = (𝐴𝐵))
5352fveq2d 6879 . . . . . . . . 9 ((𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → (𝑃 {𝐴, 𝐵}) = (𝑃‘(𝐴𝐵)))
54533ad2ant2 1134 . . . . . . . 8 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (𝑃 {𝐴, 𝐵}) = (𝑃‘(𝐴𝐵)))
55 fveq2 6875 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑃𝑥) = (𝑃𝐴))
5655adantl 482 . . . . . . . . 9 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ 𝑥 = 𝐴) → (𝑃𝑥) = (𝑃𝐴))
57 fveq2 6875 . . . . . . . . . 10 (𝑥 = 𝐵 → (𝑃𝑥) = (𝑃𝐵))
5857adantl 482 . . . . . . . . 9 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ 𝑥 = 𝐵) → (𝑃𝑥) = (𝑃𝐵))
59 unitssxrge0 32695 . . . . . . . . . 10 (0[,]1) ⊆ (0[,]+∞)
60 simp1 1136 . . . . . . . . . . 11 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → 𝑃 ∈ Prob)
61 prob01 33227 . . . . . . . . . . 11 ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃𝐴) ∈ (0[,]1))
6260, 42, 61syl2anc 584 . . . . . . . . . 10 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (𝑃𝐴) ∈ (0[,]1))
6359, 62sselid 3973 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (𝑃𝐴) ∈ (0[,]+∞))
64 prob01 33227 . . . . . . . . . . 11 ((𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃) → (𝑃𝐵) ∈ (0[,]1))
6560, 43, 64syl2anc 584 . . . . . . . . . 10 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (𝑃𝐵) ∈ (0[,]1))
6659, 65sselid 3973 . . . . . . . . 9 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → (𝑃𝐵) ∈ (0[,]+∞))
6756, 58, 42, 43, 63, 66, 44esumpr 32879 . . . . . . . 8 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → Σ*𝑥 ∈ {𝐴, 𝐵} (𝑃𝑥) = ((𝑃𝐴) +𝑒 (𝑃𝐵)))
6854, 67eqeq12d 2747 . . . . . . 7 ((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → ((𝑃 {𝐴, 𝐵}) = Σ*𝑥 ∈ {𝐴, 𝐵} (𝑃𝑥) ↔ (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) +𝑒 (𝑃𝐵))))
6968adantr 481 . . . . . 6 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → ((𝑃 {𝐴, 𝐵}) = Σ*𝑥 ∈ {𝐴, 𝐵} (𝑃𝑥) ↔ (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) +𝑒 (𝑃𝐵))))
7051, 69mpbid 231 . . . . 5 (((𝑃 ∈ Prob ∧ (𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) +𝑒 (𝑃𝐵)))
7131, 70sylanb 581 . . . 4 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) +𝑒 (𝑃𝐵)))
72 unitssre 13455 . . . . . 6 (0[,]1) ⊆ ℝ
73 simpll1 1212 . . . . . . 7 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → 𝑃 ∈ Prob)
74 simpll2 1213 . . . . . . 7 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → 𝐴 ∈ dom 𝑃)
7573, 74, 61syl2anc 584 . . . . . 6 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃𝐴) ∈ (0[,]1))
7672, 75sselid 3973 . . . . 5 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃𝐴) ∈ ℝ)
77 simpll3 1214 . . . . . . 7 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → 𝐵 ∈ dom 𝑃)
7873, 77, 64syl2anc 584 . . . . . 6 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃𝐵) ∈ (0[,]1))
7972, 78sselid 3973 . . . . 5 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃𝐵) ∈ ℝ)
80 rexadd 13190 . . . . 5 (((𝑃𝐴) ∈ ℝ ∧ (𝑃𝐵) ∈ ℝ) → ((𝑃𝐴) +𝑒 (𝑃𝐵)) = ((𝑃𝐴) + (𝑃𝐵)))
8176, 79, 80syl2anc 584 . . . 4 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → ((𝑃𝐴) +𝑒 (𝑃𝐵)) = ((𝑃𝐴) + (𝑃𝐵)))
8271, 81eqtrd 2771 . . 3 ((((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) ∧ (𝐴𝐵) = ∅) → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵)))
8382ex 413 . 2 (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) ∧ 𝐴𝐵) → ((𝐴𝐵) = ∅ → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵))))
8427, 83pm2.61dane 3028 1 ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃𝐵 ∈ dom 𝑃) → ((𝐴𝐵) = ∅ → (𝑃‘(𝐴𝐵)) = ((𝑃𝐴) + (𝑃𝐵))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2939  cdif 3938  cun 3939  cin 3940  wss 3941  c0 4315  𝒫 cpw 4593  {cpr 4621   cuni 4898  Disj wdisj 5103   class class class wbr 5138  dom cdm 5666  cfv 6529  (class class class)co 7390  ωcom 7835  cdom 8917  cr 11088  0cc0 11089  1c1 11090   + caddc 11092  +∞cpnf 11224   +𝑒 cxad 13069  [,]cicc 13306  Σ*cesum 32840  Probcprb 33221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7705  ax-inf2 9615  ax-ac2 10437  ax-cnex 11145  ax-resscn 11146  ax-1cn 11147  ax-icn 11148  ax-addcl 11149  ax-addrcl 11150  ax-mulcl 11151  ax-mulrcl 11152  ax-mulcom 11153  ax-addass 11154  ax-mulass 11155  ax-distr 11156  ax-i2m1 11157  ax-1ne0 11158  ax-1rid 11159  ax-rnegex 11160  ax-rrecex 11161  ax-cnre 11162  ax-pre-lttri 11163  ax-pre-lttrn 11164  ax-pre-ltadd 11165  ax-pre-mulgt0 11166  ax-pre-sup 11167  ax-addf 11168  ax-mulf 11169
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3430  df-v 3472  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4520  df-pw 4595  df-sn 4620  df-pr 4622  df-tp 4624  df-op 4626  df-uni 4899  df-int 4941  df-iun 4989  df-iin 4990  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6286  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6531  df-fn 6532  df-f 6533  df-f1 6534  df-fo 6535  df-f1o 6536  df-fv 6537  df-isom 6538  df-riota 7346  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7650  df-om 7836  df-1st 7954  df-2nd 7955  df-supp 8126  df-frecs 8245  df-wrecs 8276  df-recs 8350  df-rdg 8389  df-1o 8445  df-2o 8446  df-er 8683  df-map 8802  df-pm 8803  df-ixp 8872  df-en 8920  df-dom 8921  df-sdom 8922  df-fin 8923  df-fsupp 9342  df-fi 9385  df-sup 9416  df-inf 9417  df-oi 9484  df-dju 9875  df-card 9913  df-acn 9916  df-ac 10090  df-pnf 11229  df-mnf 11230  df-xr 11231  df-ltxr 11232  df-le 11233  df-sub 11425  df-neg 11426  df-div 11851  df-nn 12192  df-2 12254  df-3 12255  df-4 12256  df-5 12257  df-6 12258  df-7 12259  df-8 12260  df-9 12261  df-n0 12452  df-z 12538  df-dec 12657  df-uz 12802  df-q 12912  df-rp 12954  df-xneg 13071  df-xadd 13072  df-xmul 13073  df-ioo 13307  df-ioc 13308  df-ico 13309  df-icc 13310  df-fz 13464  df-fzo 13607  df-fl 13736  df-mod 13814  df-seq 13946  df-exp 14007  df-fac 14213  df-bc 14242  df-hash 14270  df-shft 14993  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-limsup 15394  df-clim 15411  df-rlim 15412  df-sum 15612  df-ef 15990  df-sin 15992  df-cos 15993  df-pi 15995  df-struct 17059  df-sets 17076  df-slot 17094  df-ndx 17106  df-base 17124  df-ress 17153  df-plusg 17189  df-mulr 17190  df-starv 17191  df-sca 17192  df-vsca 17193  df-ip 17194  df-tset 17195  df-ple 17196  df-ds 17198  df-unif 17199  df-hom 17200  df-cco 17201  df-rest 17347  df-topn 17348  df-0g 17366  df-gsum 17367  df-topgen 17368  df-pt 17369  df-prds 17372  df-ordt 17426  df-xrs 17427  df-qtop 17432  df-imas 17433  df-xps 17435  df-mre 17509  df-mrc 17510  df-acs 17512  df-ps 18498  df-tsr 18499  df-plusf 18539  df-mgm 18540  df-sgrp 18589  df-mnd 18600  df-mhm 18644  df-submnd 18645  df-grp 18794  df-minusg 18795  df-sbg 18796  df-mulg 18920  df-subg 18972  df-cntz 19144  df-cmn 19611  df-abl 19612  df-mgp 19944  df-ur 19961  df-ring 20013  df-cring 20014  df-subrg 20305  df-abv 20369  df-lmod 20417  df-scaf 20418  df-sra 20729  df-rgmod 20730  df-psmet 20865  df-xmet 20866  df-met 20867  df-bl 20868  df-mopn 20869  df-fbas 20870  df-fg 20871  df-cnfld 20874  df-top 22320  df-topon 22337  df-topsp 22359  df-bases 22373  df-cld 22447  df-ntr 22448  df-cls 22449  df-nei 22526  df-lp 22564  df-perf 22565  df-cn 22655  df-cnp 22656  df-haus 22743  df-tx 22990  df-hmeo 23183  df-fil 23274  df-fm 23366  df-flim 23367  df-flf 23368  df-tmd 23500  df-tgp 23501  df-tsms 23555  df-trg 23588  df-xms 23750  df-ms 23751  df-tms 23752  df-nm 24015  df-ngp 24016  df-nrg 24018  df-nlm 24019  df-ii 24317  df-cncf 24318  df-limc 25307  df-dv 25308  df-log 25989  df-esum 32841  df-siga 32922  df-meas 33009  df-prob 33222
This theorem is referenced by:  probdif  33234
  Copyright terms: Public domain W3C validator