Metamath Proof Explorer


Theorem eliccnelico

Description: An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses eliccnelico.1 φ A *
eliccnelico.b φ B *
eliccnelico.c φ C A B
eliccnelico.nel φ ¬ C A B
Assertion eliccnelico φ C = B

Proof

Step Hyp Ref Expression
1 eliccnelico.1 φ A *
2 eliccnelico.b φ B *
3 eliccnelico.c φ C A B
4 eliccnelico.nel φ ¬ C A B
5 eliccxr C A B C *
6 3 5 syl φ C *
7 iccleub A * B * C A B C B
8 1 2 3 7 syl3anc φ C B
9 1 adantr φ ¬ B C A *
10 2 adantr φ ¬ B C B *
11 6 adantr φ ¬ B C C *
12 iccgelb A * B * C A B A C
13 1 2 3 12 syl3anc φ A C
14 13 adantr φ ¬ B C A C
15 simpr φ ¬ B C ¬ B C
16 xrltnle C * B * C < B ¬ B C
17 6 2 16 syl2anc φ C < B ¬ B C
18 17 adantr φ ¬ B C C < B ¬ B C
19 15 18 mpbird φ ¬ B C C < B
20 9 10 11 14 19 elicod φ ¬ B C C A B
21 4 adantr φ ¬ B C ¬ C A B
22 20 21 condan φ B C
23 6 2 8 22 xrletrid φ C = B