leordtvallem1

		Ref	Expression
	Hypothesis	leordtval.1	$⊢ A = ran (x \in ℝ^{*} ⟼ (x, +∞])$
	Assertion	leordtvallem1	$⊢ A = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{} \| \neg y \leq x\})$

Proof

Step	Hyp	Ref	Expression
1		leordtval.1	$⊢ A = ran (x \in ℝ^{*} ⟼ (x, +∞])$
2		iocssxr	$⊢ (x, +∞] \subseteq ℝ^{*}$
3		sseqin2	$⊢ (x, +∞] \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap (x, +∞] = (x, +∞]$
4	2 3	mpbi	$⊢ ℝ^{*} \cap (x, +∞] = (x, +∞]$
5		simpl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7		elioc1	$⊢ (x \in ℝ^{} \land +∞ \in ℝ^{}) \to (y \in (x, +∞] \leftrightarrow (y \in ℝ^{*} \land x < y \land y \leq +∞))$
8	5 6 7	sylancl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in (x, +∞] \leftrightarrow (y \in ℝ^{*} \land x < y \land y \leq +∞))$
9		simpr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y \in ℝ^{*}$
10		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
11	9 10	jccir	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in ℝ^{*} \land y \leq +∞)$
12	11	biantrurd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \leftrightarrow ((y \in ℝ^{*} \land y \leq +∞) \land x < y))$
13		3anan32	$⊢ (y \in ℝ^{} \land x < y \land y \leq +∞) \leftrightarrow ((y \in ℝ^{} \land y \leq +∞) \land x < y)$
14	12 13	bitr4di	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \leftrightarrow (y \in ℝ^{*} \land x < y \land y \leq +∞))$
15		xrltnle	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \leftrightarrow \neg y \leq x)$
16	8 14 15	3bitr2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y \in (x, +∞] \leftrightarrow \neg y \leq x)$
17	16	rabbi2dva	$⊢ x \in ℝ^{} \to ℝ^{} \cap (x, +∞] = \{y \in ℝ^{*} \| \neg y \leq x\}$
18	4 17	eqtr3id	$⊢ x \in ℝ^{} \to (x, +∞] = \{y \in ℝ^{} \| \neg y \leq x\}$
19	18	mpteq2ia	$⊢ (x \in ℝ^{} ⟼ (x, +∞]) = (x \in ℝ^{} ⟼ \{y \in ℝ^{*} \| \neg y \leq x\})$
20	19	rneqi	$⊢ ran (x \in ℝ^{} ⟼ (x, +∞]) = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{*} \| \neg y \leq x\})$
21	1 20	eqtri	$⊢ A = ran (x \in ℝ^{} ⟼ \{y \in ℝ^{} \| \neg y \leq x\})$

Metamath Proof Explorer

Theorem leordtvallem1

Proof