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

Theorem coinfliprv 30863
Description: The 𝑋 we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.)
Hypotheses
Ref Expression
coinflip.h 𝐻 ∈ V
coinflip.t 𝑇 ∈ V
coinflip.th 𝐻𝑇
coinflip.2 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2)
coinflip.3 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}
Assertion
Ref Expression
coinfliprv 𝑋 ∈ (rRndVar‘𝑃)

Proof of Theorem coinfliprv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 coinflip.th . . . . . 6 𝐻𝑇
2 coinflip.h . . . . . . 7 𝐻 ∈ V
3 coinflip.t . . . . . . 7 𝑇 ∈ V
4 1ex 10315 . . . . . . 7 1 ∈ V
5 c0ex 10313 . . . . . . 7 0 ∈ V
62, 3, 4, 5fpr 6639 . . . . . 6 (𝐻𝑇 → {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}:{𝐻, 𝑇}⟶{1, 0})
71, 6ax-mp 5 . . . . 5 {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}:{𝐻, 𝑇}⟶{1, 0}
8 coinflip.3 . . . . . 6 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}
98feq1i 6241 . . . . 5 (𝑋:{𝐻, 𝑇}⟶{1, 0} ↔ {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}:{𝐻, 𝑇}⟶{1, 0})
107, 9mpbir 222 . . . 4 𝑋:{𝐻, 𝑇}⟶{1, 0}
11 coinflip.2 . . . . . 6 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2)
122, 3, 1, 11, 8coinflipuniv 30862 . . . . 5 dom 𝑃 = {𝐻, 𝑇}
1312feq2i 6242 . . . 4 (𝑋: dom 𝑃⟶{1, 0} ↔ 𝑋:{𝐻, 𝑇}⟶{1, 0})
1410, 13mpbir 222 . . 3 𝑋: dom 𝑃⟶{1, 0}
15 1re 10319 . . . . 5 1 ∈ ℝ
16 0re 10321 . . . . 5 0 ∈ ℝ
1715, 16pm3.2i 458 . . . 4 (1 ∈ ℝ ∧ 0 ∈ ℝ)
184, 5prss 4535 . . . 4 ((1 ∈ ℝ ∧ 0 ∈ ℝ) ↔ {1, 0} ⊆ ℝ)
1917, 18mpbi 221 . . 3 {1, 0} ⊆ ℝ
20 fss 6263 . . 3 ((𝑋: dom 𝑃⟶{1, 0} ∧ {1, 0} ⊆ ℝ) → 𝑋: dom 𝑃⟶ℝ)
2114, 19, 20mp2an 675 . 2 𝑋: dom 𝑃⟶ℝ
22 imassrn 5681 . . . . 5 (𝑋𝑦) ⊆ ran 𝑋
23 dfdm4 5511 . . . . . 6 dom 𝑋 = ran 𝑋
2410fdmi 6260 . . . . . 6 dom 𝑋 = {𝐻, 𝑇}
2523, 24eqtr3i 2826 . . . . 5 ran 𝑋 = {𝐻, 𝑇}
2622, 25sseqtri 3828 . . . 4 (𝑋𝑦) ⊆ {𝐻, 𝑇}
272, 3, 1, 11, 8coinflipspace 30861 . . . . . . 7 dom 𝑃 = 𝒫 {𝐻, 𝑇}
2827eleq2i 2873 . . . . . 6 ((𝑋𝑦) ∈ dom 𝑃 ↔ (𝑋𝑦) ∈ 𝒫 {𝐻, 𝑇})
29 prex 5093 . . . . . . . . 9 {⟨𝐻, 1⟩, ⟨𝑇, 0⟩} ∈ V
308, 29eqeltri 2877 . . . . . . . 8 𝑋 ∈ V
31 cnvexg 7336 . . . . . . . 8 (𝑋 ∈ V → 𝑋 ∈ V)
32 imaexg 7327 . . . . . . . 8 (𝑋 ∈ V → (𝑋𝑦) ∈ V)
3330, 31, 32mp2b 10 . . . . . . 7 (𝑋𝑦) ∈ V
3433elpw 4351 . . . . . 6 ((𝑋𝑦) ∈ 𝒫 {𝐻, 𝑇} ↔ (𝑋𝑦) ⊆ {𝐻, 𝑇})
3528, 34bitr2i 267 . . . . 5 ((𝑋𝑦) ⊆ {𝐻, 𝑇} ↔ (𝑋𝑦) ∈ dom 𝑃)
3635biimpi 207 . . . 4 ((𝑋𝑦) ⊆ {𝐻, 𝑇} → (𝑋𝑦) ∈ dom 𝑃)
3726, 36mp1i 13 . . 3 (𝑦 ∈ 𝔅 → (𝑋𝑦) ∈ dom 𝑃)
3837rgen 3106 . 2 𝑦 ∈ 𝔅 (𝑋𝑦) ∈ dom 𝑃
392, 3, 1, 11, 8coinflipprob 30860 . . . . 5 𝑃 ∈ Prob
4039a1i 11 . . . 4 (𝐻 ∈ V → 𝑃 ∈ Prob)
4140isrrvv 30824 . . 3 (𝐻 ∈ V → (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋: dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅 (𝑋𝑦) ∈ dom 𝑃)))
422, 41ax-mp 5 . 2 (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋: dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅 (𝑋𝑦) ∈ dom 𝑃))
4321, 38, 42mpbir2an 693 1 𝑋 ∈ (rRndVar‘𝑃)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wcel 2155  wne 2974  wral 3092  Vcvv 3387  wss 3763  𝒫 cpw 4345  {cpr 4366  cop 4370   cuni 4623  ccnv 5304  dom cdm 5305  ran crn 5306  cres 5307  cima 5308  wf 6091  cfv 6095  (class class class)co 6868  cr 10214  0cc0 10215  1c1 10216   / cdiv 10963  2c2 11350  chash 13331  𝑓/𝑐cofc 30476  𝔅cbrsiga 30563  Probcprb 30788  rRndVarcrrv 30821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293  ax-addf 10294  ax-mulf 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-iin 4708  df-disj 4806  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-isom 6104  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-of 7121  df-om 7290  df-1st 7392  df-2nd 7393  df-supp 7524  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-2o 7791  df-oadd 7794  df-er 7973  df-map 8088  df-pm 8089  df-ixp 8140  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-fsupp 8509  df-fi 8550  df-sup 8581  df-inf 8582  df-oi 8648  df-card 9042  df-cda 9269  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-4 11360  df-5 11361  df-6 11362  df-7 11363  df-8 11364  df-9 11365  df-n0 11554  df-xnn0 11624  df-z 11638  df-dec 11754  df-uz 11899  df-q 12002  df-rp 12041  df-xneg 12156  df-xadd 12157  df-xmul 12158  df-ioo 12391  df-ioc 12392  df-ico 12393  df-icc 12394  df-fz 12544  df-fzo 12684  df-fl 12811  df-mod 12887  df-seq 13019  df-exp 13078  df-fac 13275  df-bc 13304  df-hash 13332  df-shft 14024  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193  df-limsup 14419  df-clim 14436  df-rlim 14437  df-sum 14634  df-ef 15012  df-sin 15014  df-cos 15015  df-pi 15017  df-struct 16064  df-ndx 16065  df-slot 16066  df-base 16068  df-sets 16069  df-ress 16070  df-plusg 16160  df-mulr 16161  df-starv 16162  df-sca 16163  df-vsca 16164  df-ip 16165  df-tset 16166  df-ple 16167  df-ds 16169  df-unif 16170  df-hom 16171  df-cco 16172  df-rest 16282  df-topn 16283  df-0g 16301  df-gsum 16302  df-topgen 16303  df-pt 16304  df-prds 16307  df-ordt 16360  df-xrs 16361  df-qtop 16366  df-imas 16367  df-xps 16369  df-mre 16445  df-mrc 16446  df-acs 16448  df-ps 17399  df-tsr 17400  df-plusf 17440  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-mhm 17534  df-submnd 17535  df-grp 17624  df-minusg 17625  df-sbg 17626  df-mulg 17740  df-subg 17787  df-cntz 17945  df-cmn 18390  df-abl 18391  df-mgp 18686  df-ur 18698  df-ring 18745  df-cring 18746  df-subrg 18976  df-abv 19015  df-lmod 19063  df-scaf 19064  df-sra 19375  df-rgmod 19376  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20906  df-topon 20923  df-topsp 20945  df-bases 20958  df-cld 21031  df-ntr 21032  df-cls 21033  df-nei 21110  df-lp 21148  df-perf 21149  df-cn 21239  df-cnp 21240  df-haus 21327  df-tx 21573  df-hmeo 21766  df-fil 21857  df-fm 21949  df-flim 21950  df-flf 21951  df-tmd 22083  df-tgp 22084  df-tsms 22137  df-trg 22170  df-xms 22332  df-ms 22333  df-tms 22334  df-nm 22594  df-ngp 22595  df-nrg 22597  df-nlm 22598  df-ii 22887  df-cncf 22888  df-limc 23838  df-dv 23839  df-log 24511  df-xdiv 29945  df-esum 30409  df-ofc 30477  df-siga 30490  df-sigagen 30521  df-brsiga 30564  df-meas 30578  df-mbfm 30632  df-prob 30789  df-rrv 30822
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator