Theorem xrinfmss 6026

Description: Any subset of extended reals has an infimum.

Assertion

Ref	Expression
xrinfmss	|- (A (_ RR* -> 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 xrinfmss

Step	Hyp	Ref	Expression
1		ssxr 5513	. . 3 |- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
2		df-3or 774	. . . 4 |- ((A (_ RR \/ +oo e. A \/ -oo e. A) <-> ((A (_ RR \/ +oo e. A) \/ -oo e. A))
3		or23 263	. . . 4 |- (((A (_ RR \/ +oo e. A) \/ -oo e. A) <-> ((A (_ RR \/ -oo e. A) \/ +oo e. A))
4	2, 3	bitr 173	. . 3 |- ((A (_ RR \/ +oo e. A \/ -oo e. A) <-> ((A (_ RR \/ -oo e. A) \/ +oo e. A))
5	1, 4	sylib 198	. 2 |- (A (_ RR* -> ((A (_ RR \/ -oo e. A) \/ +oo e. A))
6		xrinfmsslem 6024	. . 3 |- ((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)))
7		ssdifss 2158	. . . . . 6 |- (A (_ RR* -> (A \ { +oo}) (_ RR*)
8		ssxr 5513	. . . . . . . 8 |- ((A \ { +oo}) (_ RR* -> ((A \ { +oo}) (_ RR \/ +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo})))
9		3orass 776	. . . . . . . . 9 |- (((A \ { +oo}) (_ RR \/ +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo})) <-> ((A \ { +oo}) (_ RR \/ ( +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo}))))
10		pnfxr 5465	. . . . . . . . . . . . . 14 |- +oo e. RR*
11	10	elisseti 1809	. . . . . . . . . . . . 13 |- +oo e. V
12	11	snid 2425	. . . . . . . . . . . 12 |- +oo e. { +oo}
13		elndif 2154	. . . . . . . . . . . 12 |- ( +oo e. { +oo} -> -. +oo e. (A \ { +oo}))
14	12, 13	ax-mp 7	. . . . . . . . . . 11 |- -. +oo e. (A \ { +oo})
15		biorf 733	. . . . . . . . . . 11 |- (-. +oo e. (A \ { +oo}) -> ( -oo e. (A \ { +oo}) <-> ( +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo}))))
16	14, 15	ax-mp 7	. . . . . . . . . 10 |- ( -oo e. (A \ { +oo}) <-> ( +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo})))
17	16	orbi2i 255	. . . . . . . . 9 |- (((A \ { +oo}) (_ RR \/ -oo e. (A \ { +oo})) <-> ((A \ { +oo}) (_ RR \/ ( +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo}))))
18	9, 17	bitr4 176	. . . . . . . 8 |- (((A \ { +oo}) (_ RR \/ +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo})) <-> ((A \ { +oo}) (_ RR \/ -oo e. (A \ { +oo})))
19	8, 18	sylib 198	. . . . . . 7 |- ((A \ { +oo}) (_ RR* -> ((A \ { +oo}) (_ RR \/ -oo e. (A \ { +oo})))
20		xrinfmsslem 6024	. . . . . . 7 |- (((A \ { +oo}) (_ RR* /\ ((A \ { +oo}) (_ RR \/ -oo e. (A \ { +oo}))) -> E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)))
21	19, 20	mpdan 702	. . . . . 6 |- ((A \ { +oo}) (_ RR* -> E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)))
22	7, 21	syl 10	. . . . 5 |- (A (_ RR* -> E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)))
23	22	adantr 389	. . . 4 |- ((A (_ RR* /\ +oo e. A) -> E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)))
24	11	snss 2452	. . . . . . . . 9 |- ( +oo e. A <-> { +oo} (_ A)
25		undif 2333	. . . . . . . . 9 |- ({ +oo} (_ A <-> ({ +oo} u. (A \ { +oo})) = A)
26		uncom 2166	. . . . . . . . . 10 |- ({ +oo} u. (A \ { +oo})) = ((A \ { +oo}) u. { +oo})
27	26	eqeq1i 1474	. . . . . . . . 9 |- (({ +oo} u. (A \ { +oo})) = A <-> ((A \ { +oo}) u. { +oo}) = A)
28	24, 25, 27	3bitr 177	. . . . . . . 8 |- ( +oo e. A <-> ((A \ { +oo}) u. { +oo}) = A)
29		raleq1 1778	. . . . . . . . 9 |- (((A \ { +oo}) u. { +oo}) = A -> (A.y e. ((A \ { +oo}) u. { +oo}) -. y < x <-> A.y e. A -. y < x))
30		rexeq1 1779	. . . . . . . . . . 11 |- (((A \ { +oo}) u. { +oo}) = A -> (E.z e. ((A \ { +oo}) u. { +oo})z < y <-> E.z e. A z < y))
31	30	imbi2d 610	. . . . . . . . . 10 |- (((A \ { +oo}) u. { +oo}) = A -> ((x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y) <-> (x < y -> E.z e. A z < y)))
32	31	ralbidv 1655	. . . . . . . . 9 |- (((A \ { +oo}) u. { +oo}) = A -> (A.y e. RR* (x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y) <-> A.y e. RR* (x < y -> E.z e. A z < y)))
33	29, 32	anbi12d 626	. . . . . . . 8 |- (((A \ { +oo}) u. { +oo}) = A -> ((A.y e. ((A \ { +oo}) u. { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y)) <-> (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
34	28, 33	sylbi 199	. . . . . . 7 |- ( +oo e. A -> ((A.y e. ((A \ { +oo}) u. { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y)) <-> (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
35	34	rexbidv 1656	. . . . . 6 |- ( +oo e. A -> (E.x e. RR* (A.y e. ((A \ { +oo}) u. { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y)) <-> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
36		xrinfmexpnf 6022	. . . . . 6 |- (E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)) -> E.x e. RR* (A.y e. ((A \ { +oo}) u. { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. ((A \ { +oo}) u. { +oo})z < y)))
37	35, 36	syl5bi 208	. . . . 5 |- ( +oo e. A -> (E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
38	37	adantl 388	. . . 4 |- ((A (_ RR* /\ +oo e. A) -> (E.x e. RR* (A.y e. (A \ { +oo}) -. y < x /\ A.y e. RR* (x < y -> E.z e. (A \ { +oo})z < y)) -> E.x e. RR* (A.y e. A -. y < x /\ A.y e. RR* (x < y -> E.z e. A z < y))))
39	23, 38	mpd 26	. . 3 |- ((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)))
40	6, 39	jaodan 426	. 2 |- ((A (_ RR* /\ ((A (_ RR \/ -oo e. A) \/ +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)))
41	5, 40	mpdan 702	1 |- (A (_ RR* -> 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 146   \/ wo 222   /\ wa 223   \/ w3o 772   = wceq 953   e. wcel 955  A.wral 1637  E.wrex 1638   \ cdif 2034   u. cun 2035   (_ wss 2037  {csn 2399   class class class wbr 2609  RRcr 5205   +oocpnf 5455   -oocmnf 5456  RR*cxr 5457   < clt 5458

This theorem is referenced by:  infmxrcl 6033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or