Theorem xrinfmsslem 6079

Description: Lemma for xrinfmss 6081.

Assertion

Ref	Expression
xrinfmsslem	|- ((A (_ RR* /\ (A (_ RR \/ -oo e. A)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))

Distinct variable group:   x,y,z,A

Proof of Theorem xrinfmsslem

Step	Hyp	Ref	Expression
1		raleq1 1789	. . . . . 6 |- (A = (/) -> (A.y e. A -. y < x <-> A.y e. (/) -. y < x))
2		rexeq1 1790	. . . . . . . 8 |- (A = (/) -> (E.z e. A z < y <-> E.z e. (/) z < y))
3	2	imbi2d 614	. . . . . . 7 |- (A = (/) -> ((x < y -> E.z e. A z < y) <-> (x < y -> E.z e. (/) z < y)))
4	3	ralbidv 1666	. . . . . 6 |- (A = (/) -> (A.y e. RR* (x < y -> E.z e. A z < y) <-> A.y e. RR* (x < y -> E.z e. (/) z < y)))
5	1, 4	anbi12d 630	. . . . 5 |- (A = (/) -> ((A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)) <-> (A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y))))
6	5	rexbidv 1667	. . . 4 |- (A = (/) -> (E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)) <-> E.x e. RR* (A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y))))
7		infm3 6056	. . . . . . . 8 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> E.x e. RR (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)))
8		rexrt 5511	. . . . . . . . . 10 |- (x e. RR -> x e. RR*)
9	8	anim1i 334	. . . . . . . . 9 |- ((x e. RR /\ (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y))) -> (x e. RR* /\ (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y))))
10	9	r19.22i2 1736	. . . . . . . 8 |- (E.x e. RR (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)))
11	7, 10	syl 10	. . . . . . 7 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)))
12		pm3.27 323	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (x < y -> E.z e. A z < y))) -> (y e. RR -> (x < y -> E.z e. A z < y)))
13		ssel 2066	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A (_ RR -> (z e. A -> z e. RR))
14		ltpnft 5554	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> z < +oo)
15	13, 14	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A (_ RR -> (z e. A -> z < +oo))
16	15	ancld 298	. . . . . . . . . . . . . . . . . . . . . 22 |- (A (_ RR -> (z e. A -> (z e. A /\ z < +oo)))
17	16	19.22dv 1292	. . . . . . . . . . . . . . . . . . . . 21 |- (A (_ RR -> (E.z z e. A -> E.z(z e. A /\ z < +oo)))
18		ne0 2292	. . . . . . . . . . . . . . . . . . . . 21 |- (A =/= (/) <-> E.z z e. A)
19		df-rex 1653	. . . . . . . . . . . . . . . . . . . . 21 |- (E.z e. A z < +oo <-> E.z(z e. A /\ z < +oo))
20	17, 18, 19	3imtr4g 555	. . . . . . . . . . . . . . . . . . . 20 |- (A (_ RR -> (A =/= (/) -> E.z e. A z < +oo))
21	20	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((A (_ RR /\ A =/= (/)) -> E.z e. A z < +oo)
22	21	a1d 12	. . . . . . . . . . . . . . . . . 18 |- ((A (_ RR /\ A =/= (/)) -> (x < +oo -> E.z e. A z < +oo))
23	22	ad2antrr 406	. . . . . . . . . . . . . . . . 17 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = +oo) -> (x < +oo -> E.z e. A z < +oo))
24		breq2 2628	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (x < y <-> x < +oo))
25		breq2 2628	. . . . . . . . . . . . . . . . . . . 20 |- (y = +oo -> (z < y <-> z < +oo))
26	25	rexbidv 1667	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (E.z e. A z < y <-> E.z e. A z < +oo))
27	24, 26	imbi12d 628	. . . . . . . . . . . . . . . . . 18 |- (y = +oo -> ((x < y -> E.z e. A z < y) <-> (x < +oo -> E.z e. A z < +oo)))
28	27	adantl 390	. . . . . . . . . . . . . . . . 17 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = +oo) -> ((x < y -> E.z e. A z < y) <-> (x < +oo -> E.z e. A z < +oo)))
29	23, 28	mpbird 196	. . . . . . . . . . . . . . . 16 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = +oo) -> (x < y -> E.z e. A z < y))
30	29	ex 373	. . . . . . . . . . . . . . 15 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (y = +oo -> (x < y -> E.z e. A z < y)))
31	30	adantr 391	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (x < y -> E.z e. A z < y))) -> (y = +oo -> (x < y -> E.z e. A z < y)))
32		nltmnft 5559	. . . . . . . . . . . . . . . . . . 19 |- (x e. RR* -> -. x < -oo)
33	32	adantr 391	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = -oo) -> -. x < -oo)
34		breq2 2628	. . . . . . . . . . . . . . . . . . . 20 |- (y = -oo -> (x < y <-> x < -oo))
35	34	negbid 613	. . . . . . . . . . . . . . . . . . 19 |- (y = -oo -> (-. x < y <-> -. x < -oo))
36	35	adantl 390	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = -oo) -> (-. x < y <-> -. x < -oo))
37	33, 36	mpbird 196	. . . . . . . . . . . . . . . . 17 |- ((x e. RR* /\ y = -oo) -> -. x < y)
38	37	pm2.21d 78	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = -oo) -> (x < y -> E.z e. A z < y))
39	38	ex 373	. . . . . . . . . . . . . . 15 |- (x e. RR* -> (y = -oo -> (x < y -> E.z e. A z < y)))
40	39	ad2antlr 407	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (x < y -> E.z e. A z < y))) -> (y = -oo -> (x < y -> E.z e. A z < y)))
41	12, 31, 40	3jaod 890	. . . . . . . . . . . . 13 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (x < y -> E.z e. A z < y))) -> ((y e. RR \/ y = +oo \/ y = -oo) -> (x < y -> E.z e. A z < y)))
42		elxr 5547	. . . . . . . . . . . . 13 |- (y e. RR* <-> (y e. RR \/ y = +oo \/ y = -oo))
43	41, 42	syl5ib 206	. . . . . . . . . . . 12 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (x < y -> E.z e. A z < y))) -> (y e. RR* -> (x < y -> E.z e. A z < y)))
44	43	ex 373	. . . . . . . . . . 11 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((y e. RR -> (x < y -> E.z e. A z < y)) -> (y e. RR* -> (x < y -> E.z e. A z < y))))
45	44	r19.20dv2 1714	. . . . . . . . . 10 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (A.y e. RR (x < y -> E.z e. A z < y) -> A.y e. RR* (x < y -> E.z e. A z < y)))
46	45	anim2d 563	. . . . . . . . 9 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)) -> (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
47	46	r19.22dva 1742	. . . . . . . 8 |- ((A (_ RR /\ A =/= (/)) -> (E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
48	47	3adant3 801	. . . . . . 7 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> (E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
49	11, 48	mpd 26	. . . . . 6 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
50	49	3expa 835	. . . . 5 |- (((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A x <_ y) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
51