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 ) } ) |