# Metamath Proof Explorer

## Theorem elioomnf

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion elioomnf ${⊢}{A}\in {ℝ}^{*}\to \left({B}\in \left(\mathrm{-\infty },{A}\right)↔\left({B}\in ℝ\wedge {B}<{A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
2 elioo2 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({B}\in \left(\mathrm{-\infty },{A}\right)↔\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\wedge {B}<{A}\right)\right)$
3 1 2 mpan ${⊢}{A}\in {ℝ}^{*}\to \left({B}\in \left(\mathrm{-\infty },{A}\right)↔\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\wedge {B}<{A}\right)\right)$
4 an32 ${⊢}\left(\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\right)\wedge {B}<{A}\right)↔\left(\left({B}\in ℝ\wedge {B}<{A}\right)\wedge \mathrm{-\infty }<{B}\right)$
5 df-3an ${⊢}\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\wedge {B}<{A}\right)↔\left(\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\right)\wedge {B}<{A}\right)$
6 mnflt ${⊢}{B}\in ℝ\to \mathrm{-\infty }<{B}$
7 6 adantr ${⊢}\left({B}\in ℝ\wedge {B}<{A}\right)\to \mathrm{-\infty }<{B}$
8 7 pm4.71i ${⊢}\left({B}\in ℝ\wedge {B}<{A}\right)↔\left(\left({B}\in ℝ\wedge {B}<{A}\right)\wedge \mathrm{-\infty }<{B}\right)$
9 4 5 8 3bitr4i ${⊢}\left({B}\in ℝ\wedge \mathrm{-\infty }<{B}\wedge {B}<{A}\right)↔\left({B}\in ℝ\wedge {B}<{A}\right)$
10 3 9 syl6bb ${⊢}{A}\in {ℝ}^{*}\to \left({B}\in \left(\mathrm{-\infty },{A}\right)↔\left({B}\in ℝ\wedge {B}<{A}\right)\right)$