Metamath Proof Explorer

Theorem elicc2

Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elicc2 ⊢A∈ℝ∧B∈ℝ→C∈AB↔C∈ℝ∧A≤C∧C≤B

Proof

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