# Metamath Proof Explorer

## Theorem elioc2

Description: Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elioc2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
2 elioc1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
3 1 2 sylan2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
4 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
5 4 a1i ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
6 simpll ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {A}\in {ℝ}^{*}$
7 simpr1 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {C}\in {ℝ}^{*}$
8 mnfle ${⊢}{A}\in {ℝ}^{*}\to \mathrm{-\infty }\le {A}$
9 8 ad2antrr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \mathrm{-\infty }\le {A}$
10 simpr2 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {A}<{C}$
11 5 6 7 9 10 xrlelttrd ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \mathrm{-\infty }<{C}$
12 1 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {B}\in {ℝ}^{*}$
13 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
14 13 a1i ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
15 simpr3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {C}\le {B}$
16 ltpnf ${⊢}{B}\in ℝ\to {B}<\mathrm{+\infty }$
17 16 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {B}<\mathrm{+\infty }$
18 7 12 14 15 17 xrlelttrd ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {C}<\mathrm{+\infty }$
19 xrrebnd ${⊢}{C}\in {ℝ}^{*}\to \left({C}\in ℝ↔\left(\mathrm{-\infty }<{C}\wedge {C}<\mathrm{+\infty }\right)\right)$
20 7 19 syl ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \left({C}\in ℝ↔\left(\mathrm{-\infty }<{C}\wedge {C}<\mathrm{+\infty }\right)\right)$
21 11 18 20 mpbir2and ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to {C}\in ℝ$
22 21 10 15 3jca ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\right)\to \left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)$
23 22 ex ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)\to \left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
24 rexr ${⊢}{C}\in ℝ\to {C}\in {ℝ}^{*}$
25 24 3anim1i ${⊢}\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\to \left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)$
26 23 25 impbid1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left(\left({C}\in {ℝ}^{*}\wedge {A}<{C}\wedge {C}\le {B}\right)↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$
27 3 26 bitrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in ℝ\right)\to \left({C}\in \left({A},{B}\right]↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}\le {B}\right)\right)$