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 ∈ A B ↔ C = A ∨ C ∈ A B ∨ C = B

Proof

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