Metamath Proof Explorer


Theorem dstfrvel

Description: Elementhood of preimage maps produced by the "less than or equal to" relation. (Contributed by Thierry Arnoux, 13-Feb-2017)

Ref Expression
Hypotheses dstfrv.1 φ P Prob
dstfrv.2 φ X RndVar P
orvclteel.1 φ A
dstfrvel.1 φ B dom P
dstfrvel.2 φ X B A
Assertion dstfrvel φ B X RV/c A

Proof

Step Hyp Ref Expression
1 dstfrv.1 φ P Prob
2 dstfrv.2 φ X RndVar P
3 orvclteel.1 φ A
4 dstfrvel.1 φ B dom P
5 dstfrvel.2 φ X B A
6 1 2 rrvvf φ X : dom P
7 6 4 ffvelrnd φ X B
8 breq1 x = X B x A X B A
9 8 elrab X B x | x A X B X B A
10 7 5 9 sylanbrc φ X B x | x A
11 6 ffund φ Fun X
12 1 2 rrvdm φ dom X = dom P
13 4 12 eleqtrrd φ B dom X
14 fvimacnv Fun X B dom X X B x | x A B X -1 x | x A
15 11 13 14 syl2anc φ X B x | x A B X -1 x | x A
16 10 15 mpbid φ B X -1 x | x A
17 1 2 3 orrvcval4 φ X RV/c A = X -1 x | x A
18 16 17 eleqtrrd φ B X RV/c A