Theorem xrinfmsslem 7286

Description: Lemma for xrinfmss 7288.

Assertion

Ref	Expression
xrinfmsslem	|- ((A C_ RR* /\ (A C_ 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		raleq 2266	. . . . . 6 |- (A = (/) -> (A.y e. A -. y < x <-> A.y e. (/) -. y < x))
2		rexeq 2267	. . . . . . . 8 |- (A = (/) -> (E.z e. A z < y <-> E.z e. (/) z < y))
3	2	imbi2d 674	. . . . . . 7 |- (A = (/) -> ((x < y -> E.z e. A z < y) <-> (x < y -> E.z e. (/) z < y)))
4	3	ralbidv 2123	. . . . . 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 690	. . . . 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 2124	. . . 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 7263	. . . . . . . 8 |- ((A C_ 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		rexr 6668	. . . . . . . . . 10 |- (x e. RR -> x e. RR*)
9	8	anim1i 361	. . . . . . . . 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	reximi2 2197	. . . . . . . 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 12	. . . . . . 7 |- ((A C_ 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		simpr 350	. . . . . . . . . . . . . 14 |- ((((A C_ 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 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A C_ RR -> (z e. A -> z e. RR))
14		ltpnf 6717	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> z < +oo)
15	13, 14	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A C_ RR -> (z e. A -> z < +oo))
16	15	ancld 322	. . . . . . . . . . . . . . . . . . . . . 22 |- (A C_ RR -> (z e. A -> (z e. A /\ z < +oo)))
17	16	eximdv 1669	. . . . . . . . . . . . . . . . . . . . 21 |- (A C_ RR -> (E.z z e. A -> E.z(z e. A /\ z < +oo)))
18		n0 2884	. . . . . . . . . . . . . . . . . . . . 21 |- (A =/= (/) <-> E.z z e. A)
19		df-rex 2110	. . . . . . . . . . . . . . . . . . . . 21 |- (E.z e. A z < +oo <-> E.z(z e. A /\ z < +oo))
20	17, 18, 19	3imtr4g 612	. . . . . . . . . . . . . . . . . . . 20 |- (A C_ RR -> (A =/= (/) -> E.z e. A z < +oo))
21	20	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((A C_ RR /\ A =/= (/)) -> E.z e. A z < +oo)
22	21	a1d 15	. . . . . . . . . . . . . . . . . 18 |- ((A C_ RR /\ A =/= (/)) -> (x < +oo -> E.z e. A z < +oo))
23	22	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((A C_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = +oo) -> (x < +oo -> E.z e. A z < +oo))
24		breq2 3342	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (x < y <-> x < +oo))
25		breq2 3342	. . . . . . . . . . . . . . . . . . . 20 |- (y = +oo -> (z < y <-> z < +oo))
26	25	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (E.z e. A z < y <-> E.z e. A z < +oo))
27	24, 26	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (y = +oo -> ((x < y -> E.z e. A z < y) <-> (x < +oo -> E.z e. A z < +oo)))
28	27	adantl 424	. . . . . . . . . . . . . . . . 17 |- ((((A C_ 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 213	. . . . . . . . . . . . . . . 16 |- ((((A C_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = +oo) -> (x < y -> E.z e. A z < y))
30	29	ex 402	. . . . . . . . . . . . . . 15 |- (((A C_ RR /\ A =/= (/)) /\ x e. RR*) -> (y = +oo -> (x < y -> E.z e. A z < y)))
31	30	adantr 425	. . . . . . . . . . . . . 14 |- ((((A C_ 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		nltmnf 6722	. . . . . . . . . . . . . . . . . . 19 |- (x e. RR* -> -. x < -oo)
33	32	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = -oo) -> -. x < -oo)
34		breq2 3342	. . . . . . . . . . . . . . . . . . . 20 |- (y = -oo -> (x < y <-> x < -oo))
35	34	notbid 673	. . . . . . . . . . . . . . . . . . 19 |- (y = -oo -> (-. x < y <-> -. x < -oo))
36	35	adantl 424	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR* /\ y = -oo) -> (-. x < y <-> -. x < -oo))
37	33, 36	mpbird 213	. . . . . . . . . . . . . . . . 17 |- ((x e. RR* /\ y = -oo) -> -. x < y)
38	37	pm2.21d 94	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = -oo) -> (x < y -> E.z e. A z < y))
39	38	ex 402	. . . . . . . . . . . . . . 15 |- (x e. RR* -> (y = -oo -> (x < y -> E.z e. A z < y)))
40	39	ad2antlr 441	. . . . . . . . . . . . . 14 |- ((((A C_ 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 1161	. . . . . . . . . . . . 13 |- ((((A C_ 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 6706	. . . . . . . . . . . . 13 |- (y e. RR* <-> (y e. RR \/ y = +oo \/ y = -oo))
43	41, 42	syl5ib 223	. . . . . . . . . . . 12 |- ((((A C_ 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 402	. . . . . . . . . . 11 |- (((A C_ 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	ralimdv2 2173	. . . . . . . . . 10 |- (((A C_ 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 620	. . . . . . . . 9 |- (((A C_ 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	reximdva 2203	. . . . . . . 8 |- ((A C_ 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 896	. . . . . . 7 |- ((A C_ 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 29	. . . . . 6 |- ((A C_ 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 1067	. . . . 5 |- (((A C_ 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		letric 6802	. . . . . . . . . . . . . . . . 17 |- ((x e. RR /\ y e. RR) -> (x <_ y \/ y <_ x))
52	51	ancoms 484	. . . . . . . . . . . . . . . 16 |- ((y e. RR /\ x e. RR) -> (x <_ y \/ y <_ x))
53	52	ord 249	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ x e. RR) -> (-. x <_ y -> y <_ x))
54		ssel2 2616	. . . . . . . . . . . . . . 15 |- ((A C_ RR /\ y e. A) -> y e. RR)
55	53, 54	sylan 497	. . . . . . . . . . . . . 14 |- (((A C_ RR /\ y e. A) /\ x e. RR) -> (-. x <_ y -> y <_ x))
56	55	an1rs 547	. . . . . . . . . . . . 13 |- (((A C_ RR /\ x e. RR) /\ y e. A) -> (-. x <_ y -> y <_ x))
57	56	reximdva 2203	. . . . . . . . . . . 12 |- ((A C_ RR /\ x e. RR) -> (E.y e. A -. x <_ y -> E.y e. A y <_ x))
58		rexnal 2114	. . . . . . . . . . . 12 |- (E.y e. A -. x <_ y <-> -. A.y e. A x <_ y)
59	57, 58	syl5ibr 224	. . . . . . . . . . 11 |- ((A C_ RR /\ x e. RR) -> (-. A.y e. A x <_ y -> E.y e. A y <_ x))
60	59	ralimdvaa 2171	. . . . . . . . . 10 |- (A C_ RR -> (A.x e. RR -. A.y e. A x <_ y -> A.x e. RR E.y e. A y <_ x))
61	60	imp 377	. . . . . . . . 9 |- ((A C_ RR /\ A.x e. RR -. A.y e. A x <_ y) -> A.x e. RR E.y e. A y <_ x)
62		ralnex 2113	. . . . . . . . 9 |- (A.x e. RR -. A.y e. A x <_ y <-> -. E.x e. RR A.y e. A x <_ y)
63	61, 62	sylan2br 502	. . . . . . . 8 |- ((A C_ RR /\ -. E.x e. RR A.y e. A x <_ y) -> A.x e. RR E.y e. A y <_ x)
64		breq1 3341	. . . . . . . . . 10 |- (y = z -> (y <_ x <-> z <_ x))
65	64	cbvrexv 2281	. . . . . . . . 9 |- (E.y e. A y <_ x <-> E.z e. A z <_ x)
66	65	ralbii 2127	. . . . . . . 8 |- (A.x e. RR E.y e. A y <_ x <-> A.x e. RR E.z e. A z <_ x)
67	63, 66	sylib 215	. . . . . . 7 |- ((A C_ RR /\ -. E.x e. RR A.y e. A x <_ y) -> A.x e. RR E.z e. A z <_ x)
68		breq2 3342	. . . . . . . . . . . 12 |- (x = -oo -> (y < x <-> y < -oo))
69	68	notbid 673	. . . . . . . . . . 11 |- (x = -oo -> (-. y < x <-> -. y < -oo))
70	69	ralbidv 2123	. . . . . . . . . 10 |- (x = -oo -> (A.y e. A -. y < x <-> A.y e. A -. y < -oo))
71		breq1 3341	. . . . . . . . . . . 12 |- (x = -oo -> (x < y <-> -oo < y))
72	71	imbi1d 675	. . . . . . . . . . 11 |- (x = -oo -> ((x < y -> E.z e. A z < y) <-> ( -oo < y -> E.z e. A z < y)))
73	72	ralbidv 2123	. . . . . . . . . 10 |- (x = -oo -> (A.y e. RR* (x < y -> E.z e. A z < y) <-> A.y e. RR* ( -oo < y -> E.z e. A z < y)))
74	70, 73	anbi12d 690	. . . . . . . . 9 |- (x = -oo -> ((A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)) <-> (A.y e. A -. y < -oo /\ A.y e. RR* ( -oo < y -> E.z e. A z < y))))
75	74	rcla4ev 2381	. . . . . . . 8 |- (( -oo e. RR* /\ (A.y e. A -. y < -oo /\ A.y e. RR* ( -oo < 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)))
76		mnfxr 6662	. . . . . . . 8 |- -oo e. RR*
77		ssel 2615	. . . . . . . . . . . 12 |- (A C_ RR -> (y e. A -> y e. RR))
78		rexr 6668	. . . . . . . . . . . . 13 |- (y e. RR -> y e. RR*)
79		nltmnf 6722	. . . . . . . . . . . . 13 |- (y e. RR* -> -. y < -oo)
80	78, 79	syl 12	. . . . . . . . . . . 12 |- (y e. RR -> -. y < -oo)
81	77, 80	syl6 25	. . . . . . . . . . 11 |- (A C_ RR -> (y e. A -> -. y < -oo))
82	81	r19.21aiv 2175	. . . . . . . . . 10 |- (A C_ RR -> A.y e. A -. y < -oo)
83	82	adantr 425	. . . . . . . . 9 |- ((A C_ RR /\ A.x e. RR E.z e. A z <_ x) -> A.y e. A -. y < -oo)
84		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (y - 1) -> (z <_ x <-> z <_ (y - 1)))
85	84	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (y - 1) -> (E.z e. A z <_ x <-> E.z e. A z <_ (y - 1)))
86	85	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . 21 |- (((y - 1) e. RR /\ A.x e. RR E.z e. A z <_ x) -> E.z e. A z <_ (y - 1))
87	86	adantrr 431	. . . . . . . . . . . . . . . . . . . 20 |- (((y - 1) e. RR /\ (A.x e. RR E.z e. A z <_ x /\ A C_ RR)) -> E.z e. A z <_ (y - 1))
88	87	ancoms 484	. . . . . . . . . . . . . . . . . . 19 |- (((A.x e. RR E.z e. A z <_ x /\ A C_ RR) /\ (y - 1) e. RR) -> E.z e. A z <_ (y - 1))
89		peano2rem 6605	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR -> (y - 1) e. RR)
90	88, 89	sylan2 500	. . . . . . . . . . . . . . . . . 18 |- (((A.x e. RR E.z e. A z <_ x /\ A C_ RR) /\ y e. RR) -> E.z e. A z <_ (y - 1))
91		ltm1 6993	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. RR -> (y - 1) < y)
92	91	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ y e. RR) -> (y - 1) < y)
93		lelttr 6693	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. RR /\ (y - 1) e. RR /\ y e. RR) -> ((z <_ (y - 1) /\ (y - 1) < y) -> z < y))
94	93	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. RR /\ ((y - 1) e. RR /\ y e. RR)) -> ((z <_ (y - 1) /\ (y - 1) < y) -> z < y))
95	89	ancri 321	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. RR -> ((y - 1) e. RR /\ y e. RR))
96	94, 95	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ y e. RR) -> ((z <_ (y - 1) /\ (y - 1) < y) -> z < y))
97	92, 96	mpan2d 766	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. RR /\ y e. RR) -> (z <_ (y - 1) -> z < y))
98		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A C_ RR /\ z e. A) -> z e. RR)
99	97, 98	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 |- (((A C_ RR /\ z e. A) /\ y e. RR) -> (z <_ (y - 1) -> z < y))
100	99	an1rs 547	. . . . . . . . . . . . . . . . . . . 20 |- (((A C_ RR /\ y e. RR) /\ z e. A) -> (z <_ (y - 1) -> z < y))
101	100	reximdva 2203	. . . . . . . . . . . . . . . . . . 19 |- ((A C_ RR /\ y e. RR) -> (E.z e. A z <_ (y - 1) -> E.z e. A z < y))
102	101	adantll 428	. . . . . . . . . . . . . . . . . 18 |- (((A.x e. RR E.z e. A z <_ x /\ A C_ RR) /\ y e. RR) -> (E.z e. A z <_ (y - 1) -> E.z e. A z < y))
103	90, 102	mpd 29	. . . . . . . . . . . . . . . . 17 |- (((A.x e. RR E.z e. A z <_ x /\ A C_ RR) /\ y e. RR) -> E.z e. A z < y)
104	103	exp31 407	. . . . . . . . . . . . . . . 16 |- (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> (y e. RR -> E.z e. A z < y)))
105	104	a1dd 53	. . . . . . . . . . . . . . 15 |- (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> (y e. RR -> E.z e. A z < y))))
106	105	com4r 45	. . . . . . . . . . . . . 14 |- (y e. RR -> (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> E.z e. A z < y))))
107	98, 14	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((A C_ RR /\ z e. A) -> z < +oo)
108	107	a1d 15	. . . . . . . . . . . . . . . . . . . 20 |- ((A C_ RR /\ z e. A) -> (z <_ 0 -> z < +oo))
109	108	reximdva 2203	. . . . . . . . . . . . . . . . . . 19 |- (A C_ RR -> (E.z e. A z <_ 0 -> E.z e. A z < +oo))
110	109	impcom 378	. . . . . . . . . . . . . . . . . 18 |- ((E.z e. A z <_ 0 /\ A C_ RR) -> E.z e. A z < +oo)
111		0re 6603	. . . . . . . . . . . . . . . . . . 19 |- 0 e. RR
112		breq2 3342	. . . . . . . . . . . . . . . . . . . . 21 |- (x = 0 -> (z <_ x <-> z <_ 0))
113	112	rexbidv 2124	. . . . . . . . . . . . . . . . . . . 20 |- (x = 0 -> (E.z e. A z <_ x <-> E.z e. A z <_ 0))
114	113	rcla4va 2378	. . . . . . . . . . . . . . . . . . 19 |- ((0 e. RR /\ A.x e. RR E.z e. A z <_ x) -> E.z e. A z <_ 0)
115	111, 114	mpan 759	. . . . . . . . . . . . . . . . . 18 |- (A.x e. RR E.z e. A z <_ x -> E.z e. A z <_ 0)
116	110, 115	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((A.x e. RR E.z e. A z <_ x /\ A C_ RR) -> E.z e. A z < +oo)
117	26, 116	syl5bir 227	. . . . . . . . . . . . . . . 16 |- (y = +oo -> ((A.x e. RR E.z e. A z <_ x /\ A C_ RR) -> E.z e. A z < y))
118	117	a1dd 53	. . . . . . . . . . . . . . 15 |- (y = +oo -> ((A.x e. RR E.z e. A z <_ x /\ A C_ RR) -> ( -oo < y -> E.z e. A z < y)))
119	118	exp3a 405	. . . . . . . . . . . . . 14 |- (y = +oo -> (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> E.z e. A z < y))))
120		xrltnr 6716	. . . . . . . . . . . . . . . . . . 19 |- ( -oo e. RR* -> -. -oo < -oo)
121	76, 120	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- -. -oo < -oo
122		breq2 3342	. . . . . . . . . . . . . . . . . 18 |- (y = -oo -> ( -oo < y <-> -oo < -oo))
123	121, 122	mtbiri 785	. . . . . . . . . . . . . . . . 17 |- (y = -oo -> -. -oo < y)
124	123	pm2.21d 94	. . . . . . . . . . . . . . . 16 |- (y = -oo -> ( -oo < y -> E.z e. A z < y))
125	124	a1d 15	. . . . . . . . . . . . . . 15 |- (y = -oo -> (A C_ RR -> ( -oo < y -> E.z e. A z < y)))
126	125	a1d 15	. . . . . . . . . . . . . 14 |- (y = -oo -> (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> E.z e. A z < y))))
127	106, 119, 126	3jaoi 1160	. . . . . . . . . . . . 13 |- ((y e. RR \/ y = +oo \/ y = -oo) -> (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> E.z e. A z < y))))
128	42, 127	sylbi 216	. . . . . . . . . . . 12 |- (y e. RR* -> (A.x e. RR E.z e. A z <_ x -> (A C_ RR -> ( -oo < y -> E.z e. A z < y))))
129	128	com13 37	. . . . . . . . . . 11 |- (A C_ RR -> (A.x e. RR E.z e. A z <_ x -> (y e. RR* -> ( -oo < y -> E.z e. A z < y))))
130	129	imp 377	. . . . . . . . . 10 |- ((A C_ RR /\ A.x e. RR E.z e. A z <_ x) -> (y e. RR* -> ( -oo < y -> E.z e. A z < y)))
131	130	r19.21aiv 2175	. . . . . . . . 9 |- ((A C_ RR /\ A.x e. RR E.z e. A z <_ x) -> A.y e. RR* ( -oo < y -> E.z e. A z < y))
132	83, 131	jca 310	. . . . . . . 8 |- ((A C_ RR /\ A.x e. RR E.z e. A z <_ x) -> (A.y e. A -. y < -oo /\ A.y e. RR* ( -oo < y -> E.z e. A z < y)))
133	75, 76, 132	sylancr 526	. . . . . . 7 |- ((A C_ RR /\ A.x e. RR E.z e. A z <_ x) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
134	67, 133	syldan 516	. . . . . 6 |- ((A C_ RR /\ -. 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)))
135	134	adantlr 429	. . . . 5 |- (((A C_ 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)))
136	50, 135	pm2.61dan 535	. . . 4 |- ((A C_ RR /\ A =/= (/)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
137		pnfxr 6660	. . . . . 6 |- +oo e. RR*
138		ral0 2974	. . . . . . 7 |- A.y e. (/) -. y < +oo
139		pnfnlt 6721	. . . . . . . . 9 |- (y e. RR* -> -. +oo < y)
140	139	pm2.21d 94	. . . . . . . 8 |- (y e. RR* -> ( +oo < y -> E.z e. (/) z < y))
141	140	rgen 2159	. . . . . . 7 |- A.y e. RR* ( +oo < y -> E.z e. (/) z < y)
142	138, 141	pm3.2i 307	. . . . . 6 |- (A.y e. (/) -. y < +oo /\ A.y e. RR* ( +oo < y -> E.z e. (/) z < y))
143		breq2 3342	. . . . . . . . . 10 |- (x = +oo -> (y < x <-> y < +oo))
144	143	notbid 673	. . . . . . . . 9 |- (x = +oo -> (-. y < x <-> -. y < +oo))
145	144	ralbidv 2123	. . . . . . . 8 |- (x = +oo -> (A.y e. (/) -. y < x <-> A.y e. (/) -. y < +oo))
146		breq1 3341	. . . . . . . . . 10 |- (x = +oo -> (x < y <-> +oo < y))
147	146	imbi1d 675	. . . . . . . . 9 |- (x = +oo -> ((x < y -> E.z e. (/) z < y) <-> ( +oo < y -> E.z e. (/) z < y)))
148	147	ralbidv 2123	. . . . . . . 8 |- (x = +oo -> (A.y e. RR* (x < y -> E.z e. (/) z < y) <-> A.y e. RR* ( +oo < y -> E.z e. (/) z < y)))
149	145, 148	anbi12d 690	. . . . . . 7 |- (x = +oo -> ((A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y)) <-> (A.y e. (/) -. y < +oo /\ A.y e. RR* ( +oo < y -> E.z e. (/) z < y))))
150	149	rcla4ev 2381	. . . . . 6 |- (( +oo e. RR* /\ (A.y e. (/) -. y < +oo /\ A.y e. RR* ( +oo < y -> E.z e. (/) z < y))) -> E.x e. RR* (A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y)))
151	137, 142, 150	mp2an 761	. . . . 5 |- E.x e. RR* (A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y))
152	151	a1i 8	. . . 4 |- (A C_ RR -> E.x e. RR* (A.y e. (/) -. y < x /\ A.y e. RR* (x < y -> E.z e. (/) z < y)))
153	6, 136, 152	pm2.61ne 2087	. . 3 |- (A C_ RR -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
154	153	adantl 424	. 2 |- ((A C_ RR* /\ A C_ RR) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y)))
155		ssel 2615	. . . . . 6 |- (A C_ RR* -> (y e. A -> y e. RR*))
156	155, 79	syl6 25	. . . . 5 |- (A C_ RR* -> (y e. A -> -. y < -oo))
157	156	r19.21aiv 2175	. . . 4 |- (A C_ RR* -> A.y e. A -. y < -oo)
158		breq1 3341	. . . . . . . 8 |- (z = -oo -> (z < y <-> -oo < y))
159	158	rcla4ev 2381	. . . . . . 7 |- (( -oo e. A /\ -oo < y) -> E.z e. A z < y)
160	159	ex 402	. . . . . 6 |- ( -oo e. A -> ( -oo < y -> E.z e. A z < y))
161	160	a1d 15	. . . . 5 |- ( -oo e. A -> (y e. RR* -> ( -oo < y -> E.z e. A z < y)))
162	161	r19.21aiv 2175	. . . 4 |- ( -oo e. A -> A.y e. RR* ( -oo < y -> E.z e. A z < y))
163	157, 162	anim12i 360	. . 3 |- ((A C_ RR* /\ -oo e. A) -> (A.y e. A -. y < -oo /\ A.y e. RR* ( -oo < y -> E.z e. A z < y)))
164	75, 76, 163	sylancr 526	. 2 |- ((A C_ 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)))
165	154, 164	jaodan 471	1 |- ((A C_ RR* /\ (A C_ 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)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106   C_ wss 2593  (/)c0 2875   class class class wbr 3338  (class class class)co 4884  RRcr 6385  0cc0 6386  1c1 6387   - cmin 6445   <_ cle 6448   +oocpnf 6650   -oocmnf 6651  RR*cxr 6652   < clt 6653

This theorem is referenced by:  xrinfmss 7288

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658

Copyright terms: Public domain