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

Theorem orvcval 30850
Description: Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.)
Hypotheses
Ref Expression
orvcval.1 (𝜑 → Fun 𝑋)
orvcval.2 (𝜑𝑋𝑉)
orvcval.3 (𝜑𝐴𝑊)
Assertion
Ref Expression
orvcval (𝜑 → (𝑋RV/𝑐𝑅𝐴) = (𝑋 “ {𝑦𝑦𝑅𝐴}))
Distinct variable groups:   𝑦,𝐴   𝑦,𝑅   𝑦,𝑋
Allowed substitution hints:   𝜑(𝑦)   𝑉(𝑦)   𝑊(𝑦)

Proof of Theorem orvcval
Dummy variables 𝑥 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-orvc 30849 . . 3 RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (𝑥 “ {𝑦𝑦𝑅𝑎}))
21a1i 11 . 2 (𝜑 → ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (𝑥 “ {𝑦𝑦𝑅𝑎})))
3 simpl 474 . . . . 5 ((𝑥 = 𝑋𝑎 = 𝐴) → 𝑥 = 𝑋)
43cnveqd 5454 . . . 4 ((𝑥 = 𝑋𝑎 = 𝐴) → 𝑥 = 𝑋)
5 simpr 479 . . . . . 6 ((𝑥 = 𝑋𝑎 = 𝐴) → 𝑎 = 𝐴)
65breq2d 4817 . . . . 5 ((𝑥 = 𝑋𝑎 = 𝐴) → (𝑦𝑅𝑎𝑦𝑅𝐴))
76abbidv 2880 . . . 4 ((𝑥 = 𝑋𝑎 = 𝐴) → {𝑦𝑦𝑅𝑎} = {𝑦𝑦𝑅𝐴})
84, 7imaeq12d 5626 . . 3 ((𝑥 = 𝑋𝑎 = 𝐴) → (𝑥 “ {𝑦𝑦𝑅𝑎}) = (𝑋 “ {𝑦𝑦𝑅𝐴}))
98adantl 473 . 2 ((𝜑 ∧ (𝑥 = 𝑋𝑎 = 𝐴)) → (𝑥 “ {𝑦𝑦𝑅𝑎}) = (𝑋 “ {𝑦𝑦𝑅𝐴}))
10 orvcval.1 . . 3 (𝜑 → Fun 𝑋)
11 orvcval.2 . . . 4 (𝜑𝑋𝑉)
12 funeq 6070 . . . . 5 (𝑥 = 𝑋 → (Fun 𝑥 ↔ Fun 𝑋))
1312elabg 3492 . . . 4 (𝑋𝑉 → (𝑋 ∈ {𝑥 ∣ Fun 𝑥} ↔ Fun 𝑋))
1411, 13syl 17 . . 3 (𝜑 → (𝑋 ∈ {𝑥 ∣ Fun 𝑥} ↔ Fun 𝑋))
1510, 14mpbird 247 . 2 (𝜑𝑋 ∈ {𝑥 ∣ Fun 𝑥})
16 orvcval.3 . . 3 (𝜑𝐴𝑊)
17 elex 3353 . . 3 (𝐴𝑊𝐴 ∈ V)
1816, 17syl 17 . 2 (𝜑𝐴 ∈ V)
19 cnvexg 7279 . . 3 (𝑋𝑉𝑋 ∈ V)
20 imaexg 7270 . . 3 (𝑋 ∈ V → (𝑋 “ {𝑦𝑦𝑅𝐴}) ∈ V)
2111, 19, 203syl 18 . 2 (𝜑 → (𝑋 “ {𝑦𝑦𝑅𝐴}) ∈ V)
222, 9, 15, 18, 21ovmpt2d 6955 1 (𝜑 → (𝑋RV/𝑐𝑅𝐴) = (𝑋 “ {𝑦𝑦𝑅𝐴}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2140  {cab 2747  Vcvv 3341   class class class wbr 4805  ccnv 5266  cima 5270  Fun wfun 6044  (class class class)co 6815  cmpt2 6817  RV/𝑐corvc 30848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-orvc 30849
This theorem is referenced by:  orvcval2  30851  orvcval4  30853
  Copyright terms: Public domain W3C validator