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

Proof

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