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

Theorem orvcelval 29675
Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.)
Hypotheses
Ref Expression
dstrvprob.1 (𝜑𝑃 ∈ Prob)
dstrvprob.2 (𝜑𝑋 ∈ (rRndVar‘𝑃))
orvcelel.1 (𝜑𝐴 ∈ 𝔅)
Assertion
Ref Expression
orvcelval (𝜑 → (𝑋RV/𝑐 E 𝐴) = (𝑋𝐴))

Proof of Theorem orvcelval
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dstrvprob.1 . . 3 (𝜑𝑃 ∈ Prob)
2 dstrvprob.2 . . 3 (𝜑𝑋 ∈ (rRndVar‘𝑃))
3 orvcelel.1 . . 3 (𝜑𝐴 ∈ 𝔅)
41, 2, 3orrvcval4 29671 . 2 (𝜑 → (𝑋RV/𝑐 E 𝐴) = (𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 E 𝐴}))
5 epelg 4844 . . . . . 6 (𝐴 ∈ 𝔅 → (𝑥 E 𝐴𝑥𝐴))
63, 5syl 17 . . . . 5 (𝜑 → (𝑥 E 𝐴𝑥𝐴))
76rabbidv 3068 . . . 4 (𝜑 → {𝑥 ∈ ℝ ∣ 𝑥 E 𝐴} = {𝑥 ∈ ℝ ∣ 𝑥𝐴})
8 dfin5 3452 . . . . 5 (ℝ ∩ 𝐴) = {𝑥 ∈ ℝ ∣ 𝑥𝐴}
98a1i 11 . . . 4 (𝜑 → (ℝ ∩ 𝐴) = {𝑥 ∈ ℝ ∣ 𝑥𝐴})
10 elssuni 4301 . . . . . . 7 (𝐴 ∈ 𝔅𝐴 𝔅)
11 unibrsiga 29383 . . . . . . 7 𝔅 = ℝ
1210, 11syl6sseq 3518 . . . . . 6 (𝐴 ∈ 𝔅𝐴 ⊆ ℝ)
133, 12syl 17 . . . . 5 (𝜑𝐴 ⊆ ℝ)
14 sseqin2 3682 . . . . 5 (𝐴 ⊆ ℝ ↔ (ℝ ∩ 𝐴) = 𝐴)
1513, 14sylib 206 . . . 4 (𝜑 → (ℝ ∩ 𝐴) = 𝐴)
167, 9, 153eqtr2d 2554 . . 3 (𝜑 → {𝑥 ∈ ℝ ∣ 𝑥 E 𝐴} = 𝐴)
1716imaeq2d 5275 . 2 (𝜑 → (𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 E 𝐴}) = (𝑋𝐴))
184, 17eqtrd 2548 1 (𝜑 → (𝑋RV/𝑐 E 𝐴) = (𝑋𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1938  {crab 2804  cin 3443  wss 3444   cuni 4270   class class class wbr 4481   E cep 4841  ccnv 4931  cima 4935  cfv 5689  (class class class)co 6425  cr 9688  𝔅cbrsiga 29378  Probcprb 29614  rRndVarcrrv 29647  RV/𝑐corvc 29662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721  ax-cnex 9745  ax-resscn 9746  ax-pre-lttri 9763  ax-pre-lttrn 9764
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-1st 6932  df-2nd 6933  df-er 7503  df-map 7620  df-en 7716  df-dom 7717  df-sdom 7718  df-pnf 9829  df-mnf 9830  df-xr 9831  df-ltxr 9832  df-le 9833  df-ioo 11915  df-topgen 15815  df-top 20428  df-bases 20429  df-esum 29224  df-siga 29305  df-sigagen 29336  df-brsiga 29379  df-meas 29393  df-mbfm 29447  df-prob 29615  df-rrv 29648  df-orvc 29663
This theorem is referenced by:  orvcelel  29676  dstrvval  29677  dstrvprob  29678
  Copyright terms: Public domain W3C validator