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	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		elicc1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
2	1	anidms	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 ∈ ( 𝐴 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
3		xrlenlt	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝐴 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐴 ) )
4		xrlenlt	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( 𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥 ) )
6		xrlttri3	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( 𝑥 = 𝐴 ↔ ( ¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥 ) ) )
7	6	biimprd	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( ( ¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥 ) → 𝑥 = 𝐴 ) )
8	7	ancoms	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( ( ¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥 ) → 𝑥 = 𝐴 ) )
9	8	expcomd	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( ¬ 𝐴 < 𝑥 → ( ¬ 𝑥 < 𝐴 → 𝑥 = 𝐴 ) ) )
10	5 9	sylbid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝑥 ≤ 𝐴 → ( ¬ 𝑥 < 𝐴 → 𝑥 = 𝐴 ) ) )
11	10	com23	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( ¬ 𝑥 < 𝐴 → ( 𝑥 ≤ 𝐴 → 𝑥 = 𝐴 ) ) )
12	3 11	sylbid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝐴 ≤ 𝑥 → ( 𝑥 ≤ 𝐴 → 𝑥 = 𝐴 ) ) )
13	12	ex	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 ∈ ℝ^* → ( 𝐴 ≤ 𝑥 → ( 𝑥 ≤ 𝐴 → 𝑥 = 𝐴 ) ) ) )
14	13	3impd	⊢ ( 𝐴 ∈ ℝ^* → ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) → 𝑥 = 𝐴 ) )
15		eleq1a	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 = 𝐴 → 𝑥 ∈ ℝ^* ) )
16		xrleid	⊢ ( 𝐴 ∈ ℝ^* → 𝐴 ≤ 𝐴 )
17		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐴 ) )
18	16 17	syl5ibrcom	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 = 𝐴 → 𝐴 ≤ 𝑥 ) )
19		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≤ 𝐴 ↔ 𝐴 ≤ 𝐴 ) )
20	16 19	syl5ibrcom	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 = 𝐴 → 𝑥 ≤ 𝐴 ) )
21	15 18 20	3jcad	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 = 𝐴 → ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
22	14 21	impbid	⊢ ( 𝐴 ∈ ℝ^* → ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ↔ 𝑥 = 𝐴 ) )
23		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
24	22 23	bitr4di	⊢ ( 𝐴 ∈ ℝ^* → ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ↔ 𝑥 ∈ { 𝐴 } ) )
25	2 24	bitrd	⊢ ( 𝐴 ∈ ℝ^* → ( 𝑥 ∈ ( 𝐴 [,] 𝐴 ) ↔ 𝑥 ∈ { 𝐴 } ) )
26	25	eqrdv	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )

Metamath Proof Explorer

Theorem iccid

Proof