Theorem ubico

Description: A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017)

	Ref	Expression
Assertion	ubico	|- ( ( A e. RR /\ B e. RR* ) -> -. B e. ( A [,) B ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( B e. RR /\ A <_ B /\ B < B ) -> B < B )
2		simp1	|- ( ( B e. RR /\ A <_ B /\ B < B ) -> B e. RR )
3	2	ltnrd	|- ( ( B e. RR /\ A <_ B /\ B < B ) -> -. B < B )
4	1 3	pm2.65i	|- -. ( B e. RR /\ A <_ B /\ B < B )
5		elico2	|- ( ( A e. RR /\ B e. RR* ) -> ( B e. ( A [,) B ) <-> ( B e. RR /\ A <_ B /\ B < B ) ) )
6	4 5	mtbiri	|- ( ( A e. RR /\ B e. RR* ) -> -. B e. ( A [,) B ) )