Metamath Proof Explorer


Theorem snunioo

Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion snunioo A*B*A<BAAB=AB

Proof

Step Hyp Ref Expression
1 simp1 A*B*A<BA*
2 iccid A*AA=A
3 1 2 syl A*B*A<BAA=A
4 3 uneq1d A*B*A<BAAAB=AAB
5 simp2 A*B*A<BB*
6 1 xrleidd A*B*A<BAA
7 simp3 A*B*A<BA<B
8 df-icc .=x*,y*z*|xzzy
9 df-ioo .=x*,y*z*|x<zz<y
10 xrltnle A*w*A<w¬wA
11 df-ico .=x*,y*z*|xzz<y
12 xrlelttr w*A*B*wAA<Bw<B
13 xrltle A*w*A<wAw
14 13 3adant1 A*A*w*A<wAw
15 14 adantld A*A*w*AAA<wAw
16 8 9 10 11 12 15 ixxun A*A*B*AAA<BAAAB=AB
17 1 1 5 6 7 16 syl32anc A*B*A<BAAAB=AB
18 4 17 eqtr3d A*B*A<BAAB=AB