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 syl6ib
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( z e. RR* /\ ( x <_ z /\ z < y ) ) -> z e. RR ) )
50 11 49 syl5bi
 |-  ( ( 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 syl6ibr
 |-  ( ( 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 ) } )