Metamath Proof Explorer

Theorem elicoelioo

Description: Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Assertion elicoelioo ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐴 ∈ ℝ* )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐵 ∈ ℝ* )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
4 elico1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
5 4 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) )
6 5 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ* )
7 1 2 3 6 syl21anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐶 ∈ ℝ* )
8 5 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ≤ 𝐶 )
9 1 2 3 8 syl21anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐴 ≤ 𝐶 )
10 1 2 jca ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
11 simprr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
12 5 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 < 𝐵 )
13 10 3 12 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐶 < 𝐵 )
14 elioo1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
15 14 notbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ¬ ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
16 15 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
17 3anan32 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ↔ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) ∧ 𝐴 < 𝐶 ) )
18 17 notbii ⊢ ( ¬ ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ↔ ¬ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) ∧ 𝐴 < 𝐶 ) )
19 imnan ⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) → ¬ 𝐴 < 𝐶 ) ↔ ¬ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) ∧ 𝐴 < 𝐶 ) )
20 18 19 bitr4i ⊢ ( ¬ ( 𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ↔ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) → ¬ 𝐴 < 𝐶 ) )
21 16 20 sylib ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) → ¬ 𝐴 < 𝐶 ) )
22 21 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 < 𝐵 ) ) → ¬ 𝐴 < 𝐶 )
23 10 11 7 13 22 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → ¬ 𝐴 < 𝐶 )
24 xeqlelt ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ ¬ 𝐴 < 𝐶 ) ) )
25 24 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐶 ∧ ¬ 𝐴 < 𝐶 ) ) → 𝐴 = 𝐶 )
26 1 7 9 23 25 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐴 = 𝐶 )
27 26 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 = 𝐶 ) )
28 eqcom ⊢ ( 𝐴 = 𝐶 ↔ 𝐶 = 𝐴 )
29 27 28 imbitrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 = 𝐴 ) )
30 pm5.6 ⊢ ( ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 = 𝐴 ) ↔ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝐶 = 𝐴 ) ) )
31 29 30 sylib ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝐶 = 𝐴 ) ) )
32 orcom ⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝐶 = 𝐴 ) ↔ ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) )
33 31 32 imbitrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) )
34 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐶 = 𝐴 )
35 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐴 ∈ ℝ* )
36 34 35 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐶 ∈ ℝ* )
37 35 xrleidd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐴 ≤ 𝐴 )
38 37 34 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐴 ≤ 𝐶 )
39 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐴 < 𝐵 )
40 34 39 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐶 < 𝐵 )
41 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐵 ∈ ℝ* )
42 35 41 4 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
43 36 38 40 42 mpbir3and ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 = 𝐴 ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
44 ioossico ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,) 𝐵 )
45 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
46 44 45 sselid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
47 43 46 jaodan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
48 47 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) )
49 33 48 impbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 = 𝐴 ∨ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) ) )