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*AA=A

Proof

Step Hyp Ref Expression
1 elicc1 A*A*xAAx*AxxA
2 1 anidms A*xAAx*AxxA
3 xrlenlt A*x*Ax¬x<A
4 xrlenlt x*A*xA¬A<x
5 4 ancoms A*x*xA¬A<x
6 xrlttri3 x*A*x=A¬x<A¬A<x
7 6 biimprd x*A*¬x<A¬A<xx=A
8 7 ancoms A*x*¬x<A¬A<xx=A
9 8 expcomd A*x*¬A<x¬x<Ax=A
10 5 9 sylbid A*x*xA¬x<Ax=A
11 10 com23 A*x*¬x<AxAx=A
12 3 11 sylbid A*x*AxxAx=A
13 12 ex A*x*AxxAx=A
14 13 3impd A*x*AxxAx=A
15 eleq1a A*x=Ax*
16 xrleid A*AA
17 breq2 x=AAxAA
18 16 17 syl5ibrcom A*x=AAx
19 breq1 x=AxAAA
20 16 19 syl5ibrcom A*x=AxA
21 15 18 20 3jcad A*x=Ax*AxxA
22 14 21 impbid A*x*AxxAx=A
23 velsn xAx=A
24 22 23 bitr4di A*x*AxxAxA
25 2 24 bitrd A*xAAxA
26 25 eqrdv A*AA=A