Metamath Proof Explorer


Theorem orvcelel

Description: Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017)

Ref Expression
Hypotheses dstrvprob.1 φ P Prob
dstrvprob.2 φ X RndVar P
orvcelel.1 φ A 𝔅
Assertion orvcelel φ X E RV/c A dom P

Proof

Step Hyp Ref Expression
1 dstrvprob.1 φ P Prob
2 dstrvprob.2 φ X RndVar P
3 orvcelel.1 φ A 𝔅
4 1 2 3 orvcelval φ X E RV/c A = X -1 A
5 1 2 rrvfinvima φ a 𝔅 X -1 a dom P
6 simpr φ a = A a = A
7 6 imaeq2d φ a = A X -1 a = X -1 A
8 7 eleq1d φ a = A X -1 a dom P X -1 A dom P
9 3 8 rspcdv φ a 𝔅 X -1 a dom P X -1 A dom P
10 5 9 mpd φ X -1 A dom P
11 4 10 eqeltrd φ X E RV/c A dom P