This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ioounsn

Description: The union of an open interval with its upper endpoint is a left-open right-closed interval. (Contributed by Jon Pennant, 8-Jun-2019)

Ref Expression
Assertion ioounsn 
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. RR* )
2 iccid 
 |-  ( B e. RR* -> ( B [,] B ) = { B } )
3 1 2 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( B [,] B ) = { B } )
4 3 uneq2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. ( B [,] B ) ) = ( ( A (,) B ) u. { B } ) )
5 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. RR* )
6 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A < B )
7 1 xrleidd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B <_ B )
8 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
9 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
10 xrlenlt 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( B <_ w <-> -. w < B ) )
11 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
12 simpl1 
 |-  ( ( ( w e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( w < B /\ B <_ B ) ) -> w e. RR* )
13 simpl2 
 |-  ( ( ( w e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( w < B /\ B <_ B ) ) -> B e. RR* )
14 simprl 
 |-  ( ( ( w e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( w < B /\ B <_ B ) ) -> w < B )
15 12 13 14 xrltled 
 |-  ( ( ( w e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( w < B /\ B <_ B ) ) -> w <_ B )
16 15 ex 
 |-  ( ( w e. RR* /\ B e. RR* /\ B e. RR* ) -> ( ( w < B /\ B <_ B ) -> w <_ B ) )
17 xrltletr 
 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A < B /\ B <_ w ) -> A < w ) )
18 8 9 10 11 16 17 ixxun 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( A < B /\ B <_ B ) ) -> ( ( A (,) B ) u. ( B [,] B ) ) = ( A (,] B ) )
19 5 1 1 6 7 18 syl32anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. ( B [,] B ) ) = ( A (,] B ) )
20 4 19 eqtr3d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )