Theorem xrge0infssOLD 28389

Description: Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019.) Obsolete version of xrge0infss 28388 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
xrge0infssOLD	|- ( A C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )

Distinct variable group:   x, y, z, A

Proof of Theorem xrge0infssOLD

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel2 3438	. . . . . . 7 |- ( ( A C_ ( 0 [,] +oo ) /\ y e. A ) -> y e. ( 0 [,] +oo ) )
2		0xr 9712	. . . . . . . . . 10 |- 0 e. RR*
3		pnfxr 11440	. . . . . . . . . 10 |- +oo e. RR*
4		iccgelb 11719	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ +oo e. RR* /\ y e. ( 0 [,] +oo ) ) -> 0 <_ y )
5	2, 3, 4	mp3an12 1363	. . . . . . . . 9 |- ( y e. ( 0 [,] +oo ) -> 0 <_ y )
6		iccssxr 11745	. . . . . . . . . . 11 |- ( 0 [,] +oo ) C_ RR*
7	6	sseli 3439	. . . . . . . . . 10 |- ( y e. ( 0 [,] +oo ) -> y e. RR* )
8		xrlenlt 9724	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ y e. RR* ) -> ( 0 <_ y <-> -. y < 0 ) )
9	2, 8	mpan 681	. . . . . . . . . 10 |- ( y e. RR* -> ( 0 <_ y <-> -. y < 0 ) )
10	7, 9	syl 17	. . . . . . . . 9 |- ( y e. ( 0 [,] +oo ) -> ( 0 <_ y <-> -. y < 0 ) )
11	5, 10	mpbid 215	. . . . . . . 8 |- ( y e. ( 0 [,] +oo ) -> -. y < 0 )
12		c0ex 9662	. . . . . . . . 9 |- 0 e. _V
13		vex 3059	. . . . . . . . 9 |- y e. _V
14	12, 13	brcnv 5035	. . . . . . . 8 |- ( 0 `' < y <-> y < 0 )
15	11, 14	sylnibr 311	. . . . . . 7 |- ( y e. ( 0 [,] +oo ) -> -. 0 `' < y )
16	1, 15	syl 17	. . . . . 6 |- ( ( A C_ ( 0 [,] +oo ) /\ y e. A ) -> -. 0 `' < y )
17	16	ralrimiva 2813	. . . . 5 |- ( A C_ ( 0 [,] +oo ) -> A. y e. A -. 0 `' < y )
18	17	ad3antrrr 741	. . . 4 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ w <_ 0 ) -> A. y e. A -. 0 `' < y )
19		ssralv 3504	. . . . . . . . . 10 |- ( ( 0 [,] +oo ) C_ RR* -> ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( w < y -> E. z e. A z < y ) ) )
20	6, 19	ax-mp 5	. . . . . . . . 9 |- ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( w < y -> E. z e. A z < y ) )
21	13, 12	brcnv 5035	. . . . . . . . . . . 12 |- ( y `' < 0 <-> 0 < y )
22		simplll 773	. . . . . . . . . . . . . 14 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> w e. RR* )
23	2	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> 0 e. RR* )
24		simplr 767	. . . . . . . . . . . . . . 15 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> y e. ( 0 [,] +oo ) )
25	6, 24	sseldi 3441	. . . . . . . . . . . . . 14 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> y e. RR* )
26		simpllr 774	. . . . . . . . . . . . . 14 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> w <_ 0 )
27		simpr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> 0 < y )
28	22, 23, 25, 26, 27	xrlelttrd 11485	. . . . . . . . . . . . 13 |- ( ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) /\ 0 < y ) -> w < y )
29	28	ex 440	. . . . . . . . . . . 12 |- ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) -> ( 0 < y -> w < y ) )
30	21, 29	syl5bi 225	. . . . . . . . . . 11 |- ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) -> ( y `' < 0 -> w < y ) )
31		vex 3059	. . . . . . . . . . . . . . 15 |- z e. _V
32	13, 31	brcnv 5035	. . . . . . . . . . . . . 14 |- ( y `' < z <-> z < y )
33	32	biimpri 211	. . . . . . . . . . . . 13 |- ( z < y -> y `' < z )
34	33	a1i 11	. . . . . . . . . . . 12 |- ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) -> ( z < y -> y `' < z ) )
35	34	reximdv 2872	. . . . . . . . . . 11 |- ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) -> ( E. z e. A z < y -> E. z e. A y `' < z ) )
36	30, 35	imim12d 77	. . . . . . . . . 10 |- ( ( ( w e. RR* /\ w <_ 0 ) /\ y e. ( 0 [,] +oo ) ) -> ( ( w < y -> E. z e. A z < y ) -> ( y `' < 0 -> E. z e. A y `' < z ) ) )
37	36	ralimdva 2807	. . . . . . . . 9 |- ( ( w e. RR* /\ w <_ 0 ) -> ( A. y e. ( 0 [,] +oo ) ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) )
38	20, 37	syl5 33	. . . . . . . 8 |- ( ( w e. RR* /\ w <_ 0 ) -> ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) )
39	38	adantll 725	. . . . . . 7 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ w <_ 0 ) -> ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) )
40	39	imp 435	. . . . . 6 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ w <_ 0 ) /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) )
41	40	adantrl 727	. . . . 5 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ w <_ 0 ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) )
42	41	an32s 818	. . . 4 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ w <_ 0 ) -> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) )
43		0e0iccpnf 11771	. . . . 5 |- 0 e. ( 0 [,] +oo )
44		breq1 4418	. . . . . . . . 9 |- ( x = 0 -> ( x `' < y <-> 0 `' < y ) )
45	44	notbid 300	. . . . . . . 8 |- ( x = 0 -> ( -. x `' < y <-> -. 0 `' < y ) )
46	45	ralbidv 2838	. . . . . . 7 |- ( x = 0 -> ( A. y e. A -. x `' < y <-> A. y e. A -. 0 `' < y ) )
47		breq2 4419	. . . . . . . . 9 |- ( x = 0 -> ( y `' < x <-> y `' < 0 ) )
48	47	imbi1d 323	. . . . . . . 8 |- ( x = 0 -> ( ( y `' < x -> E. z e. A y `' < z ) <-> ( y `' < 0 -> E. z e. A y `' < z ) ) )
49	48	ralbidv 2838	. . . . . . 7 |- ( x = 0 -> ( A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) )
50	46, 49	anbi12d 722	. . . . . 6 |- ( x = 0 -> ( ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A -. 0 `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) ) )
51	50	rspcev 3161	. . . . 5 |- ( ( 0 e. ( 0 [,] +oo ) /\ ( A. y e. A -. 0 `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
52	43, 51	mpan 681	. . . 4 |- ( ( A. y e. A -. 0 `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < 0 -> E. z e. A y `' < z ) ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
53	18, 42, 52	syl2anc 671	. . 3 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ w <_ 0 ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
54		simpllr 774	. . . . 5 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ 0 <_ w ) -> w e. RR* )
55		simpr 467	. . . . 5 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ 0 <_ w ) -> 0 <_ w )
56		elxrge0 11769	. . . . . 6 |- ( w e. ( 0 [,] +oo ) <-> ( w e. RR* /\ 0 <_ w ) )
57	56	biimpri 211	. . . . 5 |- ( ( w e. RR* /\ 0 <_ w ) -> w e. ( 0 [,] +oo ) )
58	54, 55, 57	syl2anc 671	. . . 4 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ 0 <_ w ) -> w e. ( 0 [,] +oo ) )
59		vex 3059	. . . . . . . . . . . . . 14 |- w e. _V
60	59, 13	brcnv 5035	. . . . . . . . . . . . 13 |- ( w `' < y <-> y < w )
61	60	bicomi 207	. . . . . . . . . . . 12 |- ( y < w <-> w `' < y )
62	61	a1i 11	. . . . . . . . . . 11 |- ( A C_ ( 0 [,] +oo ) -> ( y < w <-> w `' < y ) )
63	62	notbid 300	. . . . . . . . . 10 |- ( A C_ ( 0 [,] +oo ) -> ( -. y < w <-> -. w `' < y ) )
64	63	ralbidv 2838	. . . . . . . . 9 |- ( A C_ ( 0 [,] +oo ) -> ( A. y e. A -. y < w <-> A. y e. A -. w `' < y ) )
65	64	biimpd 212	. . . . . . . 8 |- ( A C_ ( 0 [,] +oo ) -> ( A. y e. A -. y < w -> A. y e. A -. w `' < y ) )
66	13, 59	brcnv 5035	. . . . . . . . . . . . 13 |- ( y `' < w <-> w < y )
67	66	biimpi 199	. . . . . . . . . . . 12 |- ( y `' < w -> w < y )
68	33	reximi 2866	. . . . . . . . . . . 12 |- ( E. z e. A z < y -> E. z e. A y `' < z )
69	67, 68	imim12i 59	. . . . . . . . . . 11 |- ( ( w < y -> E. z e. A z < y ) -> ( y `' < w -> E. z e. A y `' < z ) )
70	69	ralimi 2792	. . . . . . . . . 10 |- ( A. y e. ( 0 [,] +oo ) ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) )
71	20, 70	syl 17	. . . . . . . . 9 |- ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) )
72	71	a1i 11	. . . . . . . 8 |- ( A C_ ( 0 [,] +oo ) -> ( A. y e. RR* ( w < y -> E. z e. A z < y ) -> A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) )
73	65, 72	anim12d 570	. . . . . . 7 |- ( A C_ ( 0 [,] +oo ) -> ( ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) -> ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) ) )
74	73	adantr 471	. . . . . 6 |- ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) -> ( ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) -> ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) ) )
75	74	imp 435	. . . . 5 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) )
76	75	adantr 471	. . . 4 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ 0 <_ w ) -> ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) )
77		breq1 4418	. . . . . . . 8 |- ( x = w -> ( x `' < y <-> w `' < y ) )
78	77	notbid 300	. . . . . . 7 |- ( x = w -> ( -. x `' < y <-> -. w `' < y ) )
79	78	ralbidv 2838	. . . . . 6 |- ( x = w -> ( A. y e. A -. x `' < y <-> A. y e. A -. w `' < y ) )
80		breq2 4419	. . . . . . . 8 |- ( x = w -> ( y `' < x <-> y `' < w ) )
81	80	imbi1d 323	. . . . . . 7 |- ( x = w -> ( ( y `' < x -> E. z e. A y `' < z ) <-> ( y `' < w -> E. z e. A y `' < z ) ) )
82	81	ralbidv 2838	. . . . . 6 |- ( x = w -> ( A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) )
83	79, 82	anbi12d 722	. . . . 5 |- ( x = w -> ( ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) ) )
84	83	rspcev 3161	. . . 4 |- ( ( w e. ( 0 [,] +oo ) /\ ( A. y e. A -. w `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < w -> E. z e. A y `' < z ) ) ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
85	58, 76, 84	syl2anc 671	. . 3 |- ( ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) /\ 0 <_ w ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
86		simplr 767	. . . 4 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> w e. RR* )
87	2	a1i 11	. . . 4 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> 0 e. RR* )
88		xrletri 11478	. . . 4 |- ( ( w e. RR* /\ 0 e. RR* ) -> ( w <_ 0 \/ 0 <_ w ) )
89	86, 87, 88	syl2anc 671	. . 3 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> ( w <_ 0 \/ 0 <_ w ) )
90	53, 85, 89	mpjaodan 800	. 2 |- ( ( ( A C_ ( 0 [,] +oo ) /\ w e. RR* ) /\ ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )
91		sstr 3451	. . . 4 |- ( ( A C_ ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> A C_ RR* )
92	6, 91	mpan2 682	. . 3 |- ( A C_ ( 0 [,] +oo ) -> A C_ RR* )
93		xrinfmss 11623	. . 3 |- ( A C_ RR* -> E. w e. RR* ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) )
94	92, 93	syl 17	. 2 |- ( A C_ ( 0 [,] +oo ) -> E. w e. RR* ( A. y e. A -. y < w /\ A. y e. RR* ( w < y -> E. z e. A z < y ) ) )
95	90, 94	r19.29a 2943	1 |- ( A C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. x `' < y /\ A. y e. ( 0 [,] +oo ) ( y `' < x -> E. z e. A y `' < z ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   = wceq 1454   e. wcel 1897   A.wral 2748   E.wrex 2749   C_ wss 3415   class class class wbr 4415   `'ccnv 4851  (class class class)co 6314   0cc0 9564   +oocpnf 9697   RR*cxr 9699   < clt 9700   <_ cle 9701   [,]cicc 11666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-po 4773  df-so 4774  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-1st 6819  df-2nd 6820  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-icc 11670

This theorem is referenced by:  xrge0infssdOLD  28391  infxrge0lbOLD  28395  infxrge0glbOLD  28397  infxrge0gelbOLD  28399  omsfOLD  29172  omssubaddlemOLD  29179  omssubaddOLD  29180