Metamath Proof Explorer

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 e. RR* -> ( A [,] A ) = { A } )

Proof

Step Hyp Ref Expression
1 elicc1 
 |-  ( ( A e. RR* /\ A e. RR* ) -> ( x e. ( A [,] A ) <-> ( x e. RR* /\ A <_ x /\ x <_ A ) ) )
2 1 anidms 
 |-  ( A e. RR* -> ( x e. ( A [,] A ) <-> ( x e. RR* /\ A <_ x /\ x <_ A ) ) )
3 xrlenlt 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( A <_ x <-> -. x < A ) )
4 xrlenlt 
 |-  ( ( x e. RR* /\ A e. RR* ) -> ( x <_ A <-> -. A < x ) )
5 4 ancoms 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( x <_ A <-> -. A < x ) )
6 xrlttri3 
 |-  ( ( x e. RR* /\ A e. RR* ) -> ( x = A <-> ( -. x < A /\ -. A < x ) ) )
7 6 biimprd 
 |-  ( ( x e. RR* /\ A e. RR* ) -> ( ( -. x < A /\ -. A < x ) -> x = A ) )
8 7 ancoms 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( ( -. x < A /\ -. A < x ) -> x = A ) )
9 8 expcomd 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( -. A < x -> ( -. x < A -> x = A ) ) )
10 5 9 sylbid 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( x <_ A -> ( -. x < A -> x = A ) ) )
11 10 com23 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( -. x < A -> ( x <_ A -> x = A ) ) )
12 3 11 sylbid 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( A <_ x -> ( x <_ A -> x = A ) ) )
13 12 ex 
 |-  ( A e. RR* -> ( x e. RR* -> ( A <_ x -> ( x <_ A -> x = A ) ) ) )
14 13 3impd 
 |-  ( A e. RR* -> ( ( x e. RR* /\ A <_ x /\ x <_ A ) -> x = A ) )
15 eleq1a 
 |-  ( A e. RR* -> ( x = A -> x e. RR* ) )
16 xrleid 
 |-  ( A e. RR* -> A <_ A )
17 breq2 
 |-  ( x = A -> ( A <_ x <-> A <_ A ) )
18 16 17 syl5ibrcom 
 |-  ( A e. RR* -> ( x = A -> A <_ x ) )
19 breq1 
 |-  ( x = A -> ( x <_ A <-> A <_ A ) )
20 16 19 syl5ibrcom 
 |-  ( A e. RR* -> ( x = A -> x <_ A ) )
21 15 18 20 3jcad 
 |-  ( A e. RR* -> ( x = A -> ( x e. RR* /\ A <_ x /\ x <_ A ) ) )
22 14 21 impbid 
 |-  ( A e. RR* -> ( ( x e. RR* /\ A <_ x /\ x <_ A ) <-> x = A ) )
23 velsn 
 |-  ( x e. { A } <-> x = A )
24 22 23 bitr4di 
 |-  ( A e. RR* -> ( ( x e. RR* /\ A <_ x /\ x <_ A ) <-> x e. { A } ) )
25 2 24 bitrd 
 |-  ( A e. RR* -> ( x e. ( A [,] A ) <-> x e. { A } ) )
26 25 eqrdv 
 |-  ( A e. RR* -> ( A [,] A ) = { A } )