Theorem iooid

Description: An open interval with identical lower and upper bounds is empty. (Contributed by NM, 21-Jun-2007) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	iooid	$$⊢\left(A,A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to A\le A$$
3		ioo0	$$⊢\left(A\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(\left(A,A\right)=\varnothing \leftrightarrow A\le A\right)$$
4	2 3	mpbird	$$⊢\left(A\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(A,A\right)=\varnothing$$
5		ndmioo	$$⊢\neg \left(A\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(A,A\right)=\varnothing$$
6	4 5	pm2.61i	$$⊢\left(A,A\right)=\varnothing$$