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

Proof

Step Hyp Ref Expression
1 rexr ⊢B∈ℝ→B∈ℝ*
2 elioc1 ⊢A∈ℝ*∧B∈ℝ*→C∈AB↔C∈ℝ*∧A<C∧C≤B
3 1 2 sylan2 ⊢A∈ℝ*∧B∈ℝ→C∈AB↔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∈AB↔C∈ℝ∧A<C∧C≤B