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 ∈ ℝ * → B ∈ −∞ A ↔ B ∈ ℝ ∧ B < A

Proof

Step Hyp Ref Expression
1 mnfxr ⊢ −∞ ∈ ℝ *
2 elioo2 ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ * → B ∈ −∞ A ↔ B ∈ ℝ ∧ −∞ < B ∧ B < A
3 1 2 mpan ⊢ A ∈ ℝ * → B ∈ −∞ A ↔ B ∈ ℝ ∧ −∞ < B ∧ B < A
4 an32 ⊢ B ∈ ℝ ∧ −∞ < B ∧ B < A ↔ B ∈ ℝ ∧ B < A ∧ −∞ < B
5 df-3an ⊢ B ∈ ℝ ∧ −∞ < B ∧ B < A ↔ B ∈ ℝ ∧ −∞ < B ∧ B < A
6 mnflt ⊢ B ∈ ℝ → −∞ < B
7 6 adantr ⊢ B ∈ ℝ ∧ B < A → −∞ < B
8 7 pm4.71i ⊢ B ∈ ℝ ∧ B < A ↔ B ∈ ℝ ∧ B < A ∧ −∞ < B
9 4 5 8 3bitr4i ⊢ B ∈ ℝ ∧ −∞ < B ∧ B < A ↔ B ∈ ℝ ∧ B < A
10 3 9 bitrdi ⊢ A ∈ ℝ * → B ∈ −∞ A ↔ B ∈ ℝ ∧ B < A