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 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )

Proof

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