Metamath Proof Explorer


Theorem icoub

Description: A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion icoub A*¬BAB

Proof

Step Hyp Ref Expression
1 simpl A*BABA*
2 icossxr AB*
3 id BABBAB
4 2 3 sselid BABB*
5 4 adantl A*BABB*
6 simpr A*BABBAB
7 icoltub A*B*BABB<B
8 1 5 6 7 syl3anc A*BABB<B
9 xrltnr B*¬B<B
10 4 9 syl BAB¬B<B
11 10 adantl A*BAB¬B<B
12 8 11 pm2.65da A*¬BAB