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
|- ( ph -> P e. Prob )
dstfrv.2
|- ( ph -> X e. ( rRndVar ` P ) )
orvclteel.1
|- ( ph -> A e. RR )
dstfrvel.1
|- ( ph -> B e. U. dom P )
dstfrvel.2
|- ( ph -> ( X ` B ) <_ A )
Assertion dstfrvel
|- ( ph -> B e. ( X oRVC <_ A ) )

Proof

Step Hyp Ref Expression
1 dstfrv.1
 |-  ( ph -> P e. Prob )
2 dstfrv.2
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 orvclteel.1
 |-  ( ph -> A e. RR )
4 dstfrvel.1
 |-  ( ph -> B e. U. dom P )
5 dstfrvel.2
 |-  ( ph -> ( X ` B ) <_ A )
6 1 2 rrvvf
 |-  ( ph -> X : U. dom P --> RR )
7 6 4 ffvelrnd
 |-  ( ph -> ( X ` B ) e. RR )
8 breq1
 |-  ( x = ( X ` B ) -> ( x <_ A <-> ( X ` B ) <_ A ) )
9 8 elrab
 |-  ( ( X ` B ) e. { x e. RR | x <_ A } <-> ( ( X ` B ) e. RR /\ ( X ` B ) <_ A ) )
10 7 5 9 sylanbrc
 |-  ( ph -> ( X ` B ) e. { x e. RR | x <_ A } )
11 6 ffund
 |-  ( ph -> Fun X )
12 1 2 rrvdm
 |-  ( ph -> dom X = U. dom P )
13 4 12 eleqtrrd
 |-  ( ph -> B e. dom X )
14 fvimacnv
 |-  ( ( Fun X /\ B e. dom X ) -> ( ( X ` B ) e. { x e. RR | x <_ A } <-> B e. ( `' X " { x e. RR | x <_ A } ) ) )
15 11 13 14 syl2anc
 |-  ( ph -> ( ( X ` B ) e. { x e. RR | x <_ A } <-> B e. ( `' X " { x e. RR | x <_ A } ) ) )
16 10 15 mpbid
 |-  ( ph -> B e. ( `' X " { x e. RR | x <_ A } ) )
17 1 2 3 orrvcval4
 |-  ( ph -> ( X oRVC <_ A ) = ( `' X " { x e. RR | x <_ A } ) )
18 16 17 eleqtrrd
 |-  ( ph -> B e. ( X oRVC <_ A ) )