Metamath Proof Explorer

Theorem prunioo

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

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

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ B )
2 xrleloe 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
3 2 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
4 df-pr 
 |-  { A , B } = ( { A } u. { B } )
5 4 uneq2i 
 |-  ( ( A (,) B ) u. { A , B } ) = ( ( A (,) B ) u. ( { A } u. { B } ) )
6 unass 
 |-  ( ( ( A (,) B ) u. { A } ) u. { B } ) = ( ( A (,) B ) u. ( { A } u. { B } ) )
7 5 6 eqtr4i 
 |-  ( ( A (,) B ) u. { A , B } ) = ( ( ( A (,) B ) u. { A } ) u. { B } )
8 uncom 
 |-  ( ( A (,) B ) u. { A } ) = ( { A } u. ( A (,) B ) )
9 snunioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
10 8 9 syl5eq 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { A } ) = ( A [,) B ) )
11 10 uneq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( ( A (,) B ) u. { A } ) u. { B } ) = ( ( A [,) B ) u. { B } ) )
12 7 11 syl5eq 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { A , B } ) = ( ( A [,) B ) u. { B } ) )
13 12 3expa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A < B ) -> ( ( A (,) B ) u. { A , B } ) = ( ( A [,) B ) u. { B } ) )
14 13 3adantl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ A < B ) -> ( ( A (,) B ) u. { A , B } ) = ( ( A [,) B ) u. { B } ) )
15 snunico 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,) B ) u. { B } ) = ( A [,] B ) )
16 15 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ A < B ) -> ( ( A [,) B ) u. { B } ) = ( A [,] B ) )
17 14 16 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ A < B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
18 17 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) )
19 iccid 
 |-  ( A e. RR* -> ( A [,] A ) = { A } )
20 19 3ad2ant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A [,] A ) = { A } )
21 20 eqcomd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> { A } = ( A [,] A ) )
22 uncom 
 |-  ( (/) u. { A } ) = ( { A } u. (/) )
23 un0 
 |-  ( { A } u. (/) ) = { A }
24 22 23 eqtri 
 |-  ( (/) u. { A } ) = { A }
25 iooid 
 |-  ( A (,) A ) = (/)
26 oveq2 
 |-  ( A = B -> ( A (,) A ) = ( A (,) B ) )
27 25 26 syl5eqr 
 |-  ( A = B -> (/) = ( A (,) B ) )
28 dfsn2 
 |-  { A } = { A , A }
29 preq2 
 |-  ( A = B -> { A , A } = { A , B } )
30 28 29 syl5eq 
 |-  ( A = B -> { A } = { A , B } )
31 27 30 uneq12d 
 |-  ( A = B -> ( (/) u. { A } ) = ( ( A (,) B ) u. { A , B } ) )
32 24 31 syl5eqr 
 |-  ( A = B -> { A } = ( ( A (,) B ) u. { A , B } ) )
33 oveq2 
 |-  ( A = B -> ( A [,] A ) = ( A [,] B ) )
34 32 33 eqeq12d 
 |-  ( A = B -> ( { A } = ( A [,] A ) <-> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) )
35 21 34 syl5ibcom 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A = B -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) )
36 18 35 jaod 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A < B \/ A = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) )
37 3 36 sylbid 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A <_ B -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) )
38 1 37 mpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )