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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C ≤ B

Proof

Step Hyp Ref Expression
1 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
2 elioc1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C ≤ B
3 1 2 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C ≤ B
4 mnfxr ⊢ −∞ ∈ ℝ *
5 4 a1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → −∞ ∈ ℝ *
6 simpll ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → A ∈ ℝ *
7 simpr1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ∈ ℝ *
8 mnfle ⊢ A ∈ ℝ * → −∞ ≤ A
9 8 ad2antrr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → −∞ ≤ A
10 simpr2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → A < C
11 5 6 7 9 10 xrlelttrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → −∞ < C
12 1 ad2antlr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → B ∈ ℝ *
13 pnfxr ⊢ +∞ ∈ ℝ *
14 13 a1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → +∞ ∈ ℝ *
15 simpr3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ≤ B
16 ltpnf ⊢ B ∈ ℝ → B < +∞
17 16 ad2antlr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → B < +∞
18 7 12 14 15 17 xrlelttrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C < +∞
19 xrrebnd ⊢ C ∈ ℝ * → C ∈ ℝ ↔ −∞ < C ∧ C < +∞
20 7 19 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ∈ ℝ ↔ −∞ < C ∧ C < +∞
21 11 18 20 mpbir2and ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ∈ ℝ
22 21 10 15 3jca ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ∈ ℝ ∧ A < C ∧ C ≤ B
23 22 ex ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ ℝ * ∧ A < C ∧ C ≤ B → C ∈ ℝ ∧ A < C ∧ C ≤ B
24 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
25 24 3anim1i ⊢ C ∈ ℝ ∧ A < C ∧ C ≤ B → C ∈ ℝ * ∧ A < C ∧ C ≤ B
26 23 25 impbid1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ ℝ * ∧ A < C ∧ C ≤ B ↔ C ∈ ℝ ∧ A < C ∧ C ≤ B
27 3 26 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C ≤ B