# Metamath Proof Explorer

## Theorem leordtvallem2

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

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

### Proof

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