Theorem xrinfmss 6034

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 5521	. . 3 |- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
2		df-3or 775	. . . 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 6032	. . 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 2164	. . . . . 6 |- (A (_ RR* -> (A \ { +oo}) (_ RR*)
8		ssxr 5521	. . . . . . . 8 |- ((A \ { +oo}) (_ RR* -> ((A \ { +oo}) (_ RR \/ +oo e. (A \ { +oo}) \/ -oo e. (A \ { +oo})))
9		3orass 777	. . . . . . . . 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 5473	. . . . . . . . . . . . . 14 |- +oo e. RR*
11	10	elisseti 1814	. . . . . . . . . . . . 13 |- +oo e. V
12	11	snid 2431	. . . . . . . . . . . 12 |- +oo e. { +oo}
13		elndif 2160	. . . . . . . . . . . 12 |- ( +oo e. { +oo} -> -. +oo e. (A \ { +oo}))
14	12, 13	ax-mp 7	. . . . . . . . . . 11 |- -. +oo e. (A \ { +oo})
15		biorf 734	. . . . . . . . . . 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 6032	. . . . . . 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 703	. . . . . 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 2457	. . . . . . . . 9 |- ( +oo e. A <-> { +oo} (_ A)
25		undif 2339	. . . . . . . . 9 |- ({ +oo} (_ A <-> ({ +oo} u. (A \ { +oo})) = A)
26		uncom 2172	. . . . . . . . . 10 |- ({ +oo} u. (A \ { +oo})) = ((A \ { +oo}) u. { +oo})
27	26	eqeq1i 1479	. . . . . . . . 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 1783	. . . . . . . . 9 |- (((A \ { +oo}) u. { +oo}) = A -> (A.y e. ((A \ { +oo}) u. { +oo}) -. y < x <-> A.y e. A -. y < x))
30		rexeq1 1784	. . . . . . . . . . 11 |- (((A \ { +oo}) u. { +oo}) = A -> (E.z e. ((A \ { +oo}) u. { +oo})z < y <-> E.z e. A z < y))
31	30	imbi2d 611	. . . . . . . . . 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 1660	. . . . . . . . 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 627	. . . . . . . 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 1661	. . . . . 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 6030	. . . . . 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 703	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 773   = wceq 954   e. wcel 956  A.wral 1642  E.wrex 1643   \ cdif 2040   u. cun 2041   (_ wss 2043  {csn 2405   class class class wbr 2614  RRcr 5213   +oocpnf 5463   -oocmnf 5464  RR*cxr 5465   < clt 5466

This theorem is referenced by:  infmxrcl 6041

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

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