Metamath Proof Explorer

Theorem eliccioo

Description: Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion eliccioo ⊢A∈ℝ*∧B∈ℝ*∧A≤B→C∈AB↔C=A∨C∈AB∨C=B

Proof

Step Hyp Ref Expression
1 prunioo ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∪AB=AB
2 1 eleq2d ⊢A∈ℝ*∧B∈ℝ*∧A≤B→C∈AB∪AB↔C∈AB
3 2 biimpar ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C∈AB→C∈AB∪AB
4 elun ⊢C∈AB∪AB↔C∈AB∨C∈AB
5 elprg ⊢C∈AB→C∈AB↔C=A∨C=B
6 5 orbi2d ⊢C∈AB→C∈AB∨C∈AB↔C∈AB∨C=A∨C=B
7 4 6 bitrid ⊢C∈AB→C∈AB∪AB↔C∈AB∨C=A∨C=B
8 7 adantl ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C∈AB→C∈AB∪AB↔C∈AB∨C=A∨C=B
9 3 8 mpbid ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C∈AB→C∈AB∨C=A∨C=B
10 3orass ⊢C∈AB∨C=A∨C=B↔C∈AB∨C=A∨C=B
11 3orcoma ⊢C∈AB∨C=A∨C=B↔C=A∨C∈AB∨C=B
12 10 11 bitr3i ⊢C∈AB∨C=A∨C=B↔C=A∨C∈AB∨C=B
13 9 12 sylib ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C∈AB→C=A∨C∈AB∨C=B
14 lbicc2 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→A∈AB
15 14 adantr ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=A→A∈AB
16 eleq1 ⊢C=A→C∈AB↔A∈AB
17 16 adantl ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=A→C∈AB↔A∈AB
18 15 17 mpbird ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=A→C∈AB
19 ioossicc ⊢AB⊆AB
20 19 sseli ⊢C∈AB→C∈AB
21 20 adantl ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C∈AB→C∈AB
22 ubicc2 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→B∈AB
23 22 adantr ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=B→B∈AB
24 eleq1 ⊢C=B→C∈AB↔B∈AB
25 24 adantl ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=B→C∈AB↔B∈AB
26 23 25 mpbird ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=B→C∈AB
27 18 21 26 3jaodan ⊢A∈ℝ*∧B∈ℝ*∧A≤B∧C=A∨C∈AB∨C=B→C∈AB
28 13 27 impbida ⊢A∈ℝ*∧B∈ℝ*∧A≤B→C∈AB↔C=A∨C∈AB∨C=B