Theorem xrsupsslem 6023

Description: Lemma for xrsupss 6025.

Assertion

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

Distinct variable group:   x,y,z,A

Proof of Theorem xrsupsslem

Step	Hyp	Ref	Expression
1		raleq1 1778	. . . . . 6 |- (A = (/) -> (A.y e. A -. x < y <-> A.y e. (/) -. x < y))
2		rexeq1 1779	. . . . . . . 8 |- (A = (/) -> (E.z e. A y < z <-> E.z e. (/) y < z))
3	2	imbi2d 610	. . . . . . 7 |- (A = (/) -> ((y < x -> E.z e. A y < z) <-> (y < x -> E.z e. (/) y < z)))
4	3	ralbidv 1655	. . . . . 6 |- (A = (/) -> (A.y e. RR* (y < x -> E.z e. A y < z) <-> A.y e. RR* (y < x -> E.z e. (/) y < z)))
5	1, 4	anbi12d 626	. . . . 5 |- (A = (/) -> ((A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)) <-> (A.y e. (/) -. x < y /\ A.y e. RR* (y < x -> E.z e. (/) y < z))))
6	5	rexbidv 1656	. . . 4 |- (A = (/) -> (E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)) <-> E.x e. RR* (A.y e. (/) -. x < y /\ A.y e. RR* (y < x -> E.z e. (/) y < z))))
7		sup3 5999	. . . . . . . 8 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
8		rexrt 5471	. . . . . . . . . 10 |- (x e. RR -> x e. RR*)
9	8	anim1i 334	. . . . . . . . 9 |- ((x e. RR /\ (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))) -> (x e. RR* /\ (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
10	9	r19.22i2 1725	. . . . . . . 8 |- (E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
11	7, 10	syl 10	. . . . . . 7 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
12		pm3.27 323	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y e. RR -> (y < x -> E.z e. A y < z)))
13		pnfnltt 5519	. . . . . . . . . . . . . . . . . . 19 |- (x e. RR* -> -. +oo < x)
14	13	adantr 389	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = +oo) -> -. +oo < x)
15		breq1 2612	. . . . . . . . . . . . . . . . . . . 20 |- (y = +oo -> (y < x <-> +oo < x))
16	15	negbid 609	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (-. y < x <-> -. +oo < x))
17	16	adantl 388	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = +oo) -> (-. y < x <-> -. +oo < x))
18	14, 17	mpbird 196	. . . . . . . . . . . . . . . . 17 |- ((x e. RR* /\ y = +oo) -> -. y < x)
19	18	pm2.21d 78	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = +oo) -> (y < x -> E.z e. A y < z))
20	19	ex 373	. . . . . . . . . . . . . . 15 |- (x e. RR* -> (y = +oo -> (y < x -> E.z e. A y < z)))
21	20	ad2antlr 405	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y = +oo -> (y < x -> E.z e. A y < z)))
22		ssel 2053	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A (_ RR -> (z e. A -> z e. RR))
23		mnfltt 5516	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> -oo < z)
24	22, 23	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A (_ RR -> (z e. A -> -oo < z))
25	24	ancld 298	. . . . . . . . . . . . . . . . . . . . . 22 |- (A (_ RR -> (z e. A -> (z e. A /\ -oo < z)))
26	25	19.22dv 1285	. . . . . . . . . . . . . . . . . . . . 21 |- (A (_ RR -> (E.z z e. A -> E.z(z e. A /\ -oo < z)))
27		ne0 2278	. . . . . . . . . . . . . . . . . . . . 21 |- (A =/= (/) <-> E.z z e. A)
28		df-rex 1642	. . . . . . . . . . . . . . . . . . . . 21 |- (E.z e. A -oo < z <-> E.z(z e. A /\ -oo < z))
29	26, 27, 28	3imtr4g 551	. . . . . . . . . . . . . . . . . . . 20 |- (A (_ RR -> (A =/= (/) -> E.z e. A -oo < z))
30	29	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((A (_ RR /\ A =/= (/)) -> E.z e. A -oo < z)
31	30	a1d 12	. . . . . . . . . . . . . . . . . 18 |- ((A (_ RR /\ A =/= (/)) -> ( -oo < x -> E.z e. A -oo < z))
32	31	ad2antrr 404	. . . . . . . . . . . . . . . . 17 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> ( -oo < x -> E.z e. A -oo < z))
33		breq1 2612	. . . . . . . . . . . . . . . . . . 19 |- (y = -oo -> (y < x <-> -oo < x))
34		breq1 2612	. . . . . . . . . . . . . . . . . . . 20 |- (y = -oo -> (y < z <-> -oo < z))
35	34	rexbidv 1656	. . . . . . . . . . . . . . . . . . 19 |- (y = -oo -> (E.z e. A y < z <-> E.z e. A -oo < z))
36	33, 35	imbi12d 624	. . . . . . . . . . . . . . . . . 18 |- (y = -oo -> ((y < x -> E.z e. A y < z) <-> ( -oo < x -> E.z e. A -oo < z)))
37	36	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> ((y < x -> E.z e. A y < z) <-> ( -oo < x -> E.z e. A -oo < z)))
38	32, 37	mpbird 196	. . . . . . . . . . . . . . . 16 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> (y < x -> E.z e. A y < z))
39	38	ex 373	. . . . . . . . . . . . . . 15 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (y = -oo -> (y < x -> E.z e. A y < z)))
40	39	adantr 389	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y = -oo -> (y < x -> E.z e. A y < z)))
41	12, 21, 40	3jaod 885	. . . . . . . . . . . . 13 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> ((y e. RR \/ y = +oo \/ y = -oo) -> (y < x -> E.z e. A y < z)))
42		elxr 5508	. . . . . . . . . . . . 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 -> (y < x -> E.z e. A y < z))) -> (y e. RR* -> (y < x -> E.z e. A y < z)))
44	43	ex 373	. . . . . . . . . . 11 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((y e. RR -> (y < x -> E.z e. A y < z)) -> (y e. RR* -> (y < x -> E.z e. A y < z))))
45	44	r19.20dv2 1703	. . . . . . . . . 10 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (A.y e. RR (y < x -> E.z e. A y < z) -> A.y e. RR* (y < x -> E.z e. A y < z)))
46	45	anim2d 559	. . . . . . . . 9 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) -> (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
47	46	r19.22dva 1731	. . . . . . . 8 |- ((A (_ RR /\ A =/= (/)) -> (E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
48	47	3adant3 797	. . . . . . 7 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> (E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
49	11, 48	mpd 26	. . . . . 6 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))
50	49	3expa 831	. . . . 5 |- (((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))
51		letrit 559