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=.2
Assertion icorempo F=x,yz|xzz<y

Proof

Step Hyp Ref Expression
1 icorempo.1 F=.2
2 df-ico .=x*,y*z*|xzz<y
3 2 reseq1i .2=x*,y*z*|xzz<y2
4 ressxr *
5 resmpo **x*,y*z*|xzz<y2=x,yz*|xzz<y
6 4 4 5 mp2an x*,y*z*|xzz<y2=x,yz*|xzz<y
7 3 6 eqtri .2=x,yz*|xzz<y
8 nfv zxy
9 nfrab1 _zz*|xzz<y
10 nfrab1 _zz|xzz<y
11 rabid zz*|xzz<yz*xzz<y
12 rexr xx*
13 nltmnf x*¬x<−∞
14 12 13 syl x¬x<−∞
15 renemnf xx−∞
16 15 neneqd x¬x=−∞
17 14 16 jca x¬x<−∞¬x=−∞
18 pm4.56 ¬x<−∞¬x=−∞¬x<−∞x=−∞
19 17 18 sylib x¬x<−∞x=−∞
20 mnfxr −∞*
21 xrleloe x*−∞*x−∞x<−∞x=−∞
22 12 20 21 sylancl xx−∞x<−∞x=−∞
23 19 22 mtbird x¬x−∞
24 breq2 z=−∞xzx−∞
25 24 notbid z=−∞¬xz¬x−∞
26 23 25 syl5ibrcom xz=−∞¬xz
27 26 con2d xxz¬z=−∞
28 rexr yy*
29 pnfnlt y*¬+∞<y
30 breq1 z=+∞z<y+∞<y
31 30 notbid z=+∞¬z<y¬+∞<y
32 29 31 syl5ibrcom y*z=+∞¬z<y
33 32 con2d y*z<y¬z=+∞
34 28 33 syl yz<y¬z=+∞
35 27 34 im2anan9 xyxzz<y¬z=−∞¬z=+∞
36 35 anim2d xyz*xzz<yz*¬z=−∞¬z=+∞
37 renepnf zz+∞
38 37 neneqd z¬z=+∞
39 38 pm4.71i zz¬z=+∞
40 xrnemnf z*z−∞zz=+∞
41 40 anbi1i z*z−∞¬z=+∞zz=+∞¬z=+∞
42 df-ne z−∞¬z=−∞
43 42 anbi2i z*z−∞z*¬z=−∞
44 43 anbi1i z*z−∞¬z=+∞z*¬z=−∞¬z=+∞
45 pm5.61 zz=+∞¬z=+∞z¬z=+∞
46 41 44 45 3bitr3i z*¬z=−∞¬z=+∞z¬z=+∞
47 anass z*¬z=−∞¬z=+∞z*¬z=−∞¬z=+∞
48 39 46 47 3bitr2ri z*¬z=−∞¬z=+∞z
49 36 48 syl6ib xyz*xzz<yz
50 11 49 syl5bi xyzz*|xzz<yz
51 11 simprbi zz*|xzz<yxzz<y
52 51 a1i xyzz*|xzz<yxzz<y
53 50 52 jcad xyzz*|xzz<yzxzz<y
54 rabid zz|xzz<yzxzz<y
55 53 54 syl6ibr xyzz*|xzz<yzz|xzz<y
56 rabss2 *z|xzz<yz*|xzz<y
57 4 56 ax-mp z|xzz<yz*|xzz<y
58 57 sseli zz|xzz<yzz*|xzz<y
59 55 58 impbid1 xyzz*|xzz<yzz|xzz<y
60 8 9 10 59 eqrd xyz*|xzz<y=z|xzz<y
61 60 mpoeq3ia x,yz*|xzz<y=x,yz|xzz<y
62 1 7 61 3eqtri F=x,yz|xzz<y