orvcgteel

Description: Preimage maps produced by the "greater than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017)

	Ref	Expression
Hypotheses	orvcgteel.1	$⊢ φ \to P \in Prob$
	orvcgteel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
	orvcgteel.3	$⊢ φ \to A \in ℝ$
Assertion	orvcgteel	$⊢ φ \to X {\leq^{-1}}_{RV/c} A \in dom P$

Proof

Step	Hyp	Ref	Expression
1		orvcgteel.1	$⊢ φ \to P \in Prob$
2		orvcgteel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		orvcgteel.3	$⊢ φ \to A \in ℝ$
4		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
5	3	adantr	$⊢ (φ \land x \in ℝ) \to A \in ℝ$
6		brcnvg	$⊢ (x \in ℝ \land A \in ℝ) \to (x \leq^{-1} A \leftrightarrow A \leq x)$
7	4 5 6	syl2anc	$⊢ (φ \land x \in ℝ) \to (x \leq^{-1} A \leftrightarrow A \leq x)$
8	7	pm5.32da	$⊢ φ \to ((x \in ℝ \land x \leq^{-1} A) \leftrightarrow (x \in ℝ \land A \leq x))$
9		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
10	9	ad2antrl	$⊢ (φ \land (x \in ℝ \land A \leq x)) \to x \in ℝ^{*}$
11		simprr	$⊢ (φ \land (x \in ℝ \land A \leq x)) \to A \leq x$
12		ltpnf	$⊢ x \in ℝ \to x < +∞$
13	12	ad2antrl	$⊢ (φ \land (x \in ℝ \land A \leq x)) \to x < +∞$
14	11 13	jca	$⊢ (φ \land (x \in ℝ \land A \leq x)) \to (A \leq x \land x < +∞)$
15	10 14	jca	$⊢ (φ \land (x \in ℝ \land A \leq x)) \to (x \in ℝ^{*} \land (A \leq x \land x < +∞))$
16		simprl	$⊢ (φ \land (x \in ℝ^{} \land (A \leq x \land x < +∞))) \to x \in ℝ^{}$
17	3	adantr	$⊢ (φ \land (x \in ℝ^{*} \land (A \leq x \land x < +∞))) \to A \in ℝ$
18		simprrl	$⊢ (φ \land (x \in ℝ^{*} \land (A \leq x \land x < +∞))) \to A \leq x$
19		simprrr	$⊢ (φ \land (x \in ℝ^{*} \land (A \leq x \land x < +∞))) \to x < +∞$
20		xrre3	$⊢ ((x \in ℝ^{*} \land A \in ℝ) \land (A \leq x \land x < +∞)) \to x \in ℝ$
21	16 17 18 19 20	syl22anc	$⊢ (φ \land (x \in ℝ^{*} \land (A \leq x \land x < +∞))) \to x \in ℝ$
22	21 18	jca	$⊢ (φ \land (x \in ℝ^{*} \land (A \leq x \land x < +∞))) \to (x \in ℝ \land A \leq x)$
23	15 22	impbida	$⊢ φ \to ((x \in ℝ \land A \leq x) \leftrightarrow (x \in ℝ^{*} \land (A \leq x \land x < +∞)))$
24	8 23	bitrd	$⊢ φ \to ((x \in ℝ \land x \leq^{-1} A) \leftrightarrow (x \in ℝ^{*} \land (A \leq x \land x < +∞)))$
25	24	rabbidva2	$⊢ φ \to \{x \in ℝ \| x \leq^{-1} A\} = \{x \in ℝ^{*} \| (A \leq x \land x < +∞)\}$
26	3	rexrd	$⊢ φ \to A \in ℝ^{*}$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28		icoval	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to [A, +∞) = \{x \in ℝ^{*} \| (A \leq x \land x < +∞)\}$
29	26 27 28	sylancl	$⊢ φ \to [A, +∞) = \{x \in ℝ^{*} \| (A \leq x \land x < +∞)\}$
30	25 29	eqtr4d	$⊢ φ \to \{x \in ℝ \| x \leq^{-1} A\} = [A, +∞)$
31		icopnfcld	$⊢ A \in ℝ \to [A, +∞) \in Clsd (topGen (ran (.)))$
32	3 31	syl	$⊢ φ \to [A, +∞) \in Clsd (topGen (ran (.)))$
33	30 32	eqeltrd	$⊢ φ \to \{x \in ℝ \| x \leq^{-1} A\} \in Clsd (topGen (ran (.)))$
34	1 2 3 33	orrvccel	$⊢ φ \to X {\leq^{-1}}_{RV/c} A \in dom P$

Metamath Proof Explorer

Theorem orvcgteel

Proof