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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑋 ‘ 𝐵 ) ∈ ℝ )
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/𝑐 ≤ 𝐴 ) )