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 e. RR* -> -. B e. ( A [,) B ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> A e. RR* )
2		icossxr	|- ( A [,) B ) C_ RR*
3		id	|- ( B e. ( A [,) B ) -> B e. ( A [,) B ) )
4	2 3	sselid	|- ( B e. ( A [,) B ) -> B e. RR* )
5	4	adantl	|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B e. RR* )
6		simpr	|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B e. ( A [,) B ) )
7		icoltub	|- ( ( A e. RR* /\ B e. RR* /\ B e. ( A [,) B ) ) -> B < B )
8	1 5 6 7	syl3anc	|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> B < B )
9		xrltnr	|- ( B e. RR* -> -. B < B )
10	4 9	syl	|- ( B e. ( A [,) B ) -> -. B < B )
11	10	adantl	|- ( ( A e. RR* /\ B e. ( A [,) B ) ) -> -. B < B )
12	8 11	pm2.65da	|- ( A e. RR* -> -. B e. ( A [,) B ) )