# Metamath Proof Explorer

## Theorem leordtvallem1

Description: Lemma for leordtval . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis leordtval.1 ${⊢}{A}=\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)$
Assertion leordtvallem1 ${⊢}{A}=\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|¬{y}\le {x}\right\}\right)$

### Proof

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