Theorem iccid

Description: A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009)

	Ref	Expression
Assertion	iccid	$$⊢A\in {ℝ}^{*}\to \left[A,A\right]=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elicc1	$$⊢\left(A\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(x\in \left[A,A\right]\leftrightarrow \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\right)$$
2	1	anidms	$$⊢A\in {ℝ}^{*}\to \left(x\in \left[A,A\right]\leftrightarrow \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\right)$$
3		xrlenlt	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(A\le x\leftrightarrow \neg x<A\right)$$
4		xrlenlt	$$⊢\left(x\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(x\le A\leftrightarrow \neg A<x\right)$$
5	4	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(x\le A\leftrightarrow \neg A<x\right)$$
6		xrlttri3	$$⊢\left(x\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(x=A\leftrightarrow \left(\neg x<A\wedge \neg A<x\right)\right)$$
7	6	biimprd	$$⊢\left(x\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(\left(\neg x<A\wedge \neg A<x\right)\to x=A\right)$$
8	7	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(\left(\neg x<A\wedge \neg A<x\right)\to x=A\right)$$
9	8	expcomd	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(\neg A<x\to \left(\neg x<A\to x=A\right)\right)$$
10	5 9	sylbid	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(x\le A\to \left(\neg x<A\to x=A\right)\right)$$
11	10	com23	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(\neg x<A\to \left(x\le A\to x=A\right)\right)$$
12	3 11	sylbid	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(A\le x\to \left(x\le A\to x=A\right)\right)$$
13	12	ex	$$⊢A\in {ℝ}^{*}\to \left(x\in {ℝ}^{*}\to \left(A\le x\to \left(x\le A\to x=A\right)\right)\right)$$
14	13	3impd	$$⊢A\in {ℝ}^{*}\to \left(\left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\to x=A\right)$$
15		eleq1a	$$⊢A\in {ℝ}^{*}\to \left(x=A\to x\in {ℝ}^{*}\right)$$
16		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
17		breq2	$$⊢x=A\to \left(A\le x\leftrightarrow A\le A\right)$$
18	16 17	syl5ibrcom	$$⊢A\in {ℝ}^{*}\to \left(x=A\to A\le x\right)$$
19		breq1	$$⊢x=A\to \left(x\le A\leftrightarrow A\le A\right)$$
20	16 19	syl5ibrcom	$$⊢A\in {ℝ}^{*}\to \left(x=A\to x\le A\right)$$
21	15 18 20	3jcad	$$⊢A\in {ℝ}^{*}\to \left(x=A\to \left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\right)$$
22	14 21	impbid	$$⊢A\in {ℝ}^{*}\to \left(\left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\leftrightarrow x=A\right)$$
23		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
24	22 23	bitr4di	$$⊢A\in {ℝ}^{*}\to \left(\left(x\in {ℝ}^{*}\wedge A\le x\wedge x\le A\right)\leftrightarrow x\in \left\{A\right\}\right)$$
25	2 24	bitrd	$$⊢A\in {ℝ}^{*}\to \left(x\in \left[A,A\right]\leftrightarrow x\in \left\{A\right\}\right)$$
26	25	eqrdv	$$⊢A\in {ℝ}^{*}\to \left[A,A\right]=\left\{A\right\}$$