Metamath Proof Explorer

Theorem icorempo

Description: Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020)

Ref Expression
Hypothesis icorempo.1 
|- F = ( [,) |` ( RR X. RR ) )
Assertion icorempo 
|- F = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )

Proof

Step Hyp Ref Expression
1 icorempo.1 
 |-  F = ( [,) |` ( RR X. RR ) )
2 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
3 2 reseq1i 
 |-  ( [,) |` ( RR X. RR ) ) = ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) )
4 ressxr 
 |-  RR C_ RR*
5 resmpo 
 |-  ( ( RR C_ RR* /\ RR C_ RR* ) -> ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
6 4 4 5 mp2an 
 |-  ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
7 3 6 eqtri 
 |-  ( [,) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
8 nfv 
 |-  F/ z ( x e. RR /\ y e. RR )
9 nfrab1 
 |-  F/_ z { z e. RR* | ( x <_ z /\ z < y ) }
10 nfrab1 
 |-  F/_ z { z e. RR | ( x <_ z /\ z < y ) }
11 rabid 
 |-  ( z e. { z e. RR* | ( x <_ z /\ z < y ) } <-> ( z e. RR* /\ ( x <_ z /\ z < y ) ) )
12 rexr 
 |-  ( x e. RR -> x e. RR* )
13 nltmnf 
 |-  ( x e. RR* -> -. x < -oo )
14 12 13 syl 
 |-  ( x e. RR -> -. x < -oo )
15 renemnf 
 |-  ( x e. RR -> x =/= -oo )
16 15 neneqd 
 |-  ( x e. RR -> -. x = -oo )
17 14 16 jca 
 |-  ( x e. RR -> ( -. x < -oo /\ -. x = -oo ) )
18 pm4.56 
 |-  ( ( -. x < -oo /\ -. x = -oo ) <-> -. ( x < -oo \/ x = -oo ) )
19 17 18 sylib 
 |-  ( x e. RR -> -. ( x < -oo \/ x = -oo ) )
20 mnfxr 
 |-  -oo e. RR*
21 xrleloe 
 |-  ( ( x e. RR* /\ -oo e. RR* ) -> ( x <_ -oo <-> ( x < -oo \/ x = -oo ) ) )
22 12 20 21 sylancl 
 |-  ( x e. RR -> ( x <_ -oo <-> ( x < -oo \/ x = -oo ) ) )
23 19 22 mtbird 
 |-  ( x e. RR -> -. x <_ -oo )
24 breq2 
 |-  ( z = -oo -> ( x <_ z <-> x <_ -oo ) )
25 24 notbid 
 |-  ( z = -oo -> ( -. x <_ z <-> -. x <_ -oo ) )
26 23 25 syl5ibrcom 
 |-  ( x e. RR -> ( z = -oo -> -. x <_ z ) )
27 26 con2d 
 |-  ( x e. RR -> ( x <_ z -> -. z = -oo ) )
28 rexr 
 |-  ( y e. RR -> y e. RR* )
29 pnfnlt 
 |-  ( y e. RR* -> -. +oo < y )
30 breq1 
 |-  ( z = +oo -> ( z < y <-> +oo < y ) )
31 30 notbid 
 |-  ( z = +oo -> ( -. z < y <-> -. +oo < y ) )
32 29 31 syl5ibrcom 
 |-  ( y e. RR* -> ( z = +oo -> -. z < y ) )
33 32 con2d 
 |-  ( y e. RR* -> ( z < y -> -. z = +oo ) )
34 28 33 syl 
 |-  ( y e. RR -> ( z < y -> -. z = +oo ) )
35 27 34 im2anan9 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x <_ z /\ z < y ) -> ( -. z = -oo /\ -. z = +oo ) ) )
36 35 anim2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( z e. RR* /\ ( x <_ z /\ z < y ) ) -> ( z e. RR* /\ ( -. z = -oo /\ -. z = +oo ) ) ) )
37 renepnf 
 |-  ( z e. RR -> z =/= +oo )
38 37 neneqd 
 |-  ( z e. RR -> -. z = +oo )
39 38 pm4.71i 
 |-  ( z e. RR <-> ( z e. RR /\ -. z = +oo ) )
40 xrnemnf 
 |-  ( ( z e. RR* /\ z =/= -oo ) <-> ( z e. RR \/ z = +oo ) )
41 40 anbi1i 
 |-  ( ( ( z e. RR* /\ z =/= -oo ) /\ -. z = +oo ) <-> ( ( z e. RR \/ z = +oo ) /\ -. z = +oo ) )
42 df-ne 
 |-  ( z =/= -oo <-> -. z = -oo )
43 42 anbi2i 
 |-  ( ( z e. RR* /\ z =/= -oo ) <-> ( z e. RR* /\ -. z = -oo ) )
44 43 anbi1i 
 |-  ( ( ( z e. RR* /\ z =/= -oo ) /\ -. z = +oo ) <-> ( ( z e. RR* /\ -. z = -oo ) /\ -. z = +oo ) )
45 pm5.61 
 |-  ( ( ( z e. RR \/ z = +oo ) /\ -. z = +oo ) <-> ( z e. RR /\ -. z = +oo ) )
46 41 44 45 3bitr3i 
 |-  ( ( ( z e. RR* /\ -. z = -oo ) /\ -. z = +oo ) <-> ( z e. RR /\ -. z = +oo ) )
47 anass 
 |-  ( ( ( z e. RR* /\ -. z = -oo ) /\ -. z = +oo ) <-> ( z e. RR* /\ ( -. z = -oo /\ -. z = +oo ) ) )
48 39 46 47 3bitr2ri 
 |-  ( ( z e. RR* /\ ( -. z = -oo /\ -. z = +oo ) ) <-> z e. RR )
49 36 48 imbitrdi 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( z e. RR* /\ ( x <_ z /\ z < y ) ) -> z e. RR ) )
50 11 49 biimtrid 
 |-  ( ( x e. RR /\ y e. RR ) -> ( z e. { z e. RR* | ( x <_ z /\ z < y ) } -> z e. RR ) )
51 11 simprbi 
 |-  ( z e. { z e. RR* | ( x <_ z /\ z < y ) } -> ( x <_ z /\ z < y ) )
52 51 a1i 
 |-  ( ( x e. RR /\ y e. RR ) -> ( z e. { z e. RR* | ( x <_ z /\ z < y ) } -> ( x <_ z /\ z < y ) ) )
53 50 52 jcad 
 |-  ( ( x e. RR /\ y e. RR ) -> ( z e. { z e. RR* | ( x <_ z /\ z < y ) } -> ( z e. RR /\ ( x <_ z /\ z < y ) ) ) )
54 rabid 
 |-  ( z e. { z e. RR | ( x <_ z /\ z < y ) } <-> ( z e. RR /\ ( x <_ z /\ z < y ) ) )
55 53 54 imbitrrdi 
 |-  ( ( x e. RR /\ y e. RR ) -> ( z e. { z e. RR* | ( x <_ z /\ z < y ) } -> z e. { z e. RR | ( x <_ z /\ z < y ) } ) )
56 rabss2 
 |-  ( RR C_ RR* -> { z e. RR | ( x <_ z /\ z < y ) } C_ { z e. RR* | ( x <_ z /\ z < y ) } )
57 4 56 ax-mp 
 |-  { z e. RR | ( x <_ z /\ z < y ) } C_ { z e. RR* | ( x <_ z /\ z < y ) }
58 57 sseli 
 |-  ( z e. { z e. RR | ( x <_ z /\ z < y ) } -> z e. { z e. RR* | ( x <_ z /\ z < y ) } )
59 55 58 impbid1 
 |-  ( ( x e. RR /\ y e. RR ) -> ( z e. { z e. RR* | ( x <_ z /\ z < y ) } <-> z e. { z e. RR | ( x <_ z /\ z < y ) } ) )
60 8 9 10 59 eqrd 
 |-  ( ( x e. RR /\ y e. RR ) -> { z e. RR* | ( x <_ z /\ z < y ) } = { z e. RR | ( x <_ z /\ z < y ) } )
61 60 mpoeq3ia 
 |-  ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )
62 1 7 61 3eqtri 
 |-  F = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )