leordtvallem2

	Ref	Expression
Hypotheses	leordtval.1	$⊢ A = ran (x \in ℝ^{*} ⟼ (x, +∞])$
	leordtval.2	$⊢ B = ran (x \in ℝ^{*} ⟼ [−∞, x))$
Assertion	leordtvallem2	$⊢ B = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{} \| \neg x \leq y\})$

Proof

Step	Hyp	Ref	Expression
1		leordtval.1	$⊢ A = ran (x \in ℝ^{*} ⟼ (x, +∞])$
2		leordtval.2	$⊢ B = ran (x \in ℝ^{*} ⟼ [−∞, x))$
3		icossxr	$⊢ [−∞, x) \subseteq ℝ^{*}$
4		sseqin2	$⊢ [−∞, x) \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap [−∞, x) = [−∞, x)$
5	3 4	mpbi	$⊢ ℝ^{*} \cap [−∞, x) = [−∞, x)$
6		mnfxr	$⊢ −∞ \in ℝ^{*}$
7		simpl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x \in ℝ^{*}$
8		elico1	$⊢ (−∞ \in ℝ^{} \land x \in ℝ^{}) \to (y \in [−∞, x) \leftrightarrow (y \in ℝ^{*} \land −∞ \leq y \land y < x))$
9	6 7 8	sylancr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in [−∞, x) \leftrightarrow (y \in ℝ^{*} \land −∞ \leq y \land y < x))$
10		simpr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y \in ℝ^{*}$
11		mnfle	$⊢ y \in ℝ^{*} \to −∞ \leq y$
12	10 11	jccir	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in ℝ^{*} \land −∞ \leq y)$
13	12	biantrurd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y < x \leftrightarrow ((y \in ℝ^{*} \land −∞ \leq y) \land y < x))$
14		df-3an	$⊢ (y \in ℝ^{} \land −∞ \leq y \land y < x) \leftrightarrow ((y \in ℝ^{} \land −∞ \leq y) \land y < x)$
15	13 14	bitr4di	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y < x \leftrightarrow (y \in ℝ^{*} \land −∞ \leq y \land y < x))$
16		xrltnle	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to (y < x \leftrightarrow \neg x \leq y)$
17	16	ancoms	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y < x \leftrightarrow \neg x \leq y)$
18	9 15 17	3bitr2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in [−∞, x) \leftrightarrow \neg x \leq y)$
19	18	rabbi2dva	$⊢ x \in ℝ^{} \to ℝ^{} \cap [−∞, x) = \{y \in ℝ^{*} \| \neg x \leq y\}$
20	5 19	eqtr3id	$⊢ x \in ℝ^{} \to [−∞, x) = \{y \in ℝ^{} \| \neg x \leq y\}$
21	20	mpteq2ia	$⊢ (x \in ℝ^{} ⟼ [−∞, x)) = (x \in ℝ^{} ⟼ \{y \in ℝ^{*} \| \neg x \leq y\})$
22	21	rneqi	$⊢ ran (x \in ℝ^{} ⟼ [−∞, x)) = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{*} \| \neg x \leq y\})$
23	2 22	eqtri	$⊢ B = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{} \| \neg x \leq y\})$

Metamath Proof Explorer

Theorem leordtvallem2

Proof