Metamath Proof Explorer

Theorem elicopnf

Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion elicopnf ⊢ A ∈ ℝ → B ∈ A +∞ ↔ B ∈ ℝ ∧ A ≤ B

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ *
2 elico2 ⊢ A ∈ ℝ ∧ +∞ ∈ ℝ * → B ∈ A +∞ ↔ B ∈ ℝ ∧ A ≤ B ∧ B < +∞
3 1 2 mpan2 ⊢ A ∈ ℝ → B ∈ A +∞ ↔ B ∈ ℝ ∧ A ≤ B ∧ B < +∞
4 ltpnf ⊢ B ∈ ℝ → B < +∞
5 4 adantr ⊢ B ∈ ℝ ∧ A ≤ B → B < +∞
6 5 pm4.71i ⊢ B ∈ ℝ ∧ A ≤ B ↔ B ∈ ℝ ∧ A ≤ B ∧ B < +∞
7 df-3an ⊢ B ∈ ℝ ∧ A ≤ B ∧ B < +∞ ↔ B ∈ ℝ ∧ A ≤ B ∧ B < +∞
8 6 7 bitr4i ⊢ B ∈ ℝ ∧ A ≤ B ↔ B ∈ ℝ ∧ A ≤ B ∧ B < +∞
9 3 8 syl6bbr ⊢ A ∈ ℝ → B ∈ A +∞ ↔ B ∈ ℝ ∧ A ≤ B