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 ( 𝜑𝑃 ∈ Prob )
dstfrv.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
orvclteel.1 ( 𝜑𝐴 ∈ ℝ )
dstfrvel.1 ( 𝜑𝐵 dom 𝑃 )
dstfrvel.2 ( 𝜑 → ( 𝑋𝐵 ) ≤ 𝐴 )
Assertion dstfrvel ( 𝜑𝐵 ∈ ( 𝑋RV/𝑐𝐴 ) )

Proof

Step Hyp Ref Expression
1 dstfrv.1 ( 𝜑𝑃 ∈ Prob )
2 dstfrv.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 orvclteel.1 ( 𝜑𝐴 ∈ ℝ )
4 dstfrvel.1 ( 𝜑𝐵 dom 𝑃 )
5 dstfrvel.2 ( 𝜑 → ( 𝑋𝐵 ) ≤ 𝐴 )
6 1 2 rrvvf ( 𝜑𝑋 : dom 𝑃 ⟶ ℝ )
7 6 4 ffvelrnd ( 𝜑 → ( 𝑋𝐵 ) ∈ ℝ )
8 breq1 ( 𝑥 = ( 𝑋𝐵 ) → ( 𝑥𝐴 ↔ ( 𝑋𝐵 ) ≤ 𝐴 ) )
9 8 elrab ( ( 𝑋𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ↔ ( ( 𝑋𝐵 ) ∈ ℝ ∧ ( 𝑋𝐵 ) ≤ 𝐴 ) )
10 7 5 9 sylanbrc ( 𝜑 → ( 𝑋𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } )
11 6 ffund ( 𝜑 → Fun 𝑋 )
12 1 2 rrvdm ( 𝜑 → dom 𝑋 = dom 𝑃 )
13 4 12 eleqtrrd ( 𝜑𝐵 ∈ dom 𝑋 )
14 fvimacnv ( ( Fun 𝑋𝐵 ∈ dom 𝑋 ) → ( ( 𝑋𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ↔ 𝐵 ∈ ( 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ) ) )
15 11 13 14 syl2anc ( 𝜑 → ( ( 𝑋𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ↔ 𝐵 ∈ ( 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ) ) )
16 10 15 mpbid ( 𝜑𝐵 ∈ ( 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ) )
17 1 2 3 orrvcval4 ( 𝜑 → ( 𝑋RV/𝑐𝐴 ) = ( 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥𝐴 } ) )
18 16 17 eleqtrrd ( 𝜑𝐵 ∈ ( 𝑋RV/𝑐𝐴 ) )