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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → C ∈ A B ↔ C = A ∨ C ∈ A B

Proof

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