Theorem infmsup 6025

Description: The infimum (expressed as supremum with converse 'less-than') of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound.

Assertion

Ref	Expression
infmsup	|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> sup(A, RR, `' < ) = -usup({z e. RR | -uz e. A}, RR, < ))

Distinct variable group:   x,y,z,A

Proof of Theorem infmsup

Step	Hyp	Ref	Expression
1		infm3 6011	. . . 4 |- ((A (_ 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.w e. A w < y)))
2	1	3exp 831	. . 3 |- (A (_ 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.w e. A w < y)))))
3		breq2 2619	. . . . . . . . . . 11 |- (x = -uv -> (y < x <-> y < -uv))
4	3	negbid 610	. . . . . . . . . 10 |- (x = -uv -> (-. y < x <-> -. y < -uv))
5	4	ralbidv 1661	. . . . . . . . 9 |- (x = -uv -> (A.y e. A -. y < x <-> A.y e. A -. y < -uv))
6		breq1 2618	. . . . . . . . . . 11 |- (x = -uv -> (x < y <-> -uv < y))
7	6	imbi1d 612	. . . . . . . . . 10 |- (x = -uv -> ((x < y -> E.w e. A w < y) <-> (-uv < y -> E.w e. A w < y)))
8	7	ralbidv 1661	. . . . . . . . 9 |- (x = -uv -> (A.y e. RR (x < y -> E.w e. A w < y) <-> A.y e. RR (-uv < y -> E.w e. A w < y)))
9	5, 8	anbi12d 627	. . . . . . . 8 |- (x = -uv -> ((A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y)) <-> (A.y e. A -. y < -uv /\ A.y e. RR (-uv < y -> E.w e. A w < y))))
10	9	reuunineg 6023	. . . . . . 7 |- (E!x e. RR (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y)) -> U.{x e. RR | (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y))} = -uU.{v e. RR | (A.y e. A -. y < -uv /\ A.y e. RR (-uv < y -> E.w e. A w < y))})
11		df-sup 4557	. . . . . . . 8 |- sup(A, RR, `' < ) = U.{x e. RR | (A.y e. A -. x`' < y /\ A.y e. RR (y`' < x -> E.w e. A y`' < w))}
12		visset 1810	. . . . . . . . . . . . . . 15 |- x e. V
13		visset 1810	. . . . . . . . . . . . . . 15 |- y e. V
14	12, 13	brcnv 3295	. . . . . . . . . . . . . 14 |- (x`' < y <-> y < x)
15	14	negbii 187	. . . . . . . . . . . . 13 |- (-. x`' < y <-> -. y < x)
16	15	ralbii 1665	. . . . . . . . . . . 12 |- (A.y e. A -. x`' < y <-> A.y e. A -. y < x)
17	13, 12	brcnv 3295	. . . . . . . . . . . . . 14 |- (y`' < x <-> x < y)
18		visset 1810	. . . . . . . . . . . . . . . 16 |- w e. V
19	13, 18	brcnv 3295	. . . . . . . . . . . . . . 15 |- (y`' < w <-> w < y)
20	19	rexbii 1666	. . . . . . . . . . . . . 14 |- (E.w e. A y`' < w <-> E.w e. A w < y)
21	17, 20	imbi12i 188	. . . . . . . . . . . . 13 |- ((y`' < x -> E.w e. A y`' < w) <-> (x < y -> E.w e. A w < y))
22	21	ralbii 1665	. . . . . . . . . . . 12 |- (A.y e. RR (y`' < x -> E.w e. A y`' < w) <-> A.y e. RR (x < y -> E.w e. A w < y))
23	16, 22	anbi12i 482	. . . . . . . . . . 11 |- ((A.y e. A -. x`' < y /\ A.y e. RR (y`' < x -> E.w e. A y`' < w)) <-> (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y)))
24	23	a1i 8	. . . . . . . . . 10 |- (x e. RR -> ((A.y e. A -. x`' < y /\ A.y e. RR (y`' < x -> E.w e. A y`' < w)) <-> (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y))))
25	24	rabbii 1802	. . . . . . . . 9 |- {x e. RR | (A.y e. A -. x`' < y /\ A.y e. RR (y`' < x -> E.w e. A y`' < w))} = {x e. RR | (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y))}
26	25	unieqi 2507	. . . . . . . 8 |- U.{x e. RR | (A.y e. A -. x`' < y /\ A.y e. RR (y`' < x -> E.w e. A y`' < w))} = U.{x e. RR | (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y))}
27	11, 26	eqtr 1493	. . . . . . 7 |- sup(A, RR, `' < ) = U.{x e. RR | (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y))}
28	10, 27	syl5eq 1517	. . . . . 6 |- (E!x e. RR (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.w e. A w < y)) -> sup(A, RR, `' < ) = -uU.{v e. RR | (A.y e. A -. y < -uv /\ A.y e. RR (-uv < y -> E.w e. A w < y))})
29		ltnegt 5638	. . . . . . . . . . . . . . . . 17 |- ((v e. RR /\ u e. RR) -> (v < u <-> -uu < -uv))
30	29	negbid 610	. . . . . . . . . . . . . . . 16 |- ((v e. RR /\ u e. RR) -> (-. v < u <-> -. -uu < -uv))
31	30	imbi2d 611	. . . . . . . . . . . . . . 15 |- ((v e. RR /\ u e. RR) -> ((-uu e. A -> -. v < u) <-> (-uu e. A -> -. -uu < -uv)))
32	31	ralbidva 1657	. . . . . . . . . . . . . 14 |- (v e. RR -> (A.u e. RR (-uu e. A -> -. v < u) <-> A.u e. RR (-uu e. A -> -. -uu < -uv)))
33		negeq 5342	. . . . . . . . . . . . . . . . . . . 20 |- (z = u -> -uz = -uu)
34	33	eleq1d 1538	. . . . . . . . . . . . . . . . . . 19 |- (z = u -> (-uz e. A <-> -uu e. A))
35	34	elrab 1902	. . . . . . . . . . . . . . . . . 18 |- (u e. {z e. RR | -uz e. A} <-> (u e. RR /\ -uu e. A))
36	35	imbi1i 186	. . . . . . . . . . . . . . . . 17 |- ((u e. {z e. RR | -uz e. A} -> -. v < u) <-> ((u e. RR /\ -uu e. A) -> -. v < u))
37		impexp 347	. . . . . . . . . . . . . . . . 17 |- (((u e. RR /\ -uu e. A) -> -. v < u) <-> (u e. RR -> (-uu e. A -> -. v < u)))
38	36, 37	bitr 173	. . . . . . . . . . . . . . . 16 |- ((u e. {z e. RR | -uz e. A} -> -. v < u) <-> (u e. RR -> (-uu e. A -> -. v < u)))
39	38	albii 998	. . . . . . . . . . . . . . 15 |- (A.u(u e. {z e. RR | -uz e. A} -> -. v < u) <-> A.u(u e. RR -> (-uu e. A -> -. v < u)))
40		df-ral 1647	. . . . . . . . . . . . . . 15 |- (A.u e. {z e. RR | -uz e. A} -. v < u <-> A.u(u e. {z e. RR | -uz e. A} -> -. v < u))
41		df-ral 1647	. . . . . . . . . . . . . . 15 |- (A.u e. RR (-uu e. A -> -. v < u) <-> A.u(u e. RR -> (-uu e. A -> -. v < u)))
42	39, 40, 41	3bitr4r 184	. . . . . . . . . . . . . 14 |- (A.u e. RR (-uu e. A -> -. v < u) <-> A.u e. {z e. RR | -uz e. A} -. v < u)
43	32, 42	syl5bbr 533	. . . . . . . . . . . . 13 |- (v e. RR -> (A.u e. {z e. RR | -uz e. A} -. v < u <-> A.u e. RR (-uu e. A -> -. -uu < -uv)))
44		ltnegt 5638	. . . . . . . . . . . . . . . 16 |- ((u e. RR /\ v e. RR) -> (u < v <-> -uv < -uu))
45	44	ancoms 436	. . . . . . . . . . . . . . 15 |- ((v e. RR /\ u e. RR) -> (u < v <-> -uv < -uu))
46		ltnegt 5638	. . . . . . . . . . . . . . . . . . 19 |- ((u e. RR /\ t e. RR) -> (u < t <-> -ut < -uu))
47	46	anbi2d 615	. . . . . . . . . . . . . . . . . 18 |- ((u e. RR /\ t e. RR) -> ((-ut e. A /\ u < t) <-> (-ut e. A /\ -ut < -uu)))
48	47	rexbidva 1658	. . . . . . . . . . . . . . . . 17 |- (u e. RR -> (E.t e. RR (-ut e. A /\ u < t) <-> E.t e. RR (-ut e. A /\ -ut < -uu)))
49		negeq 5342	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = t -> -uz = -ut)
50	49	eleq1d 1538	. . . . . . . . . . . . . . . . . . . . 21 |- (z = t -> (-uz e. A <-> -ut e. A))
51	50	elrab 1902	. . . . . . . . . . . . . . . . . . . 20 |- (t e. {z e. RR | -uz e. A} <-> (t e. RR /\ -ut e. A))
52	51	anbi1i 481	. . . . . . . . . . . . . . . . . . 19 |- ((t e. {z e. RR | -uz e. A} /\ u < t) <-> ((t e. RR /\ -ut e. A) /\ u < t))
53		anass 439	. . . . . . . . . . . . . . . . . . 19 |- (((t e. RR /\ -ut e. A) /\ u < t) <-> (t e. RR /\ (-ut e. A /\ u < t)))
54	52, 53	bitr 173	. . . . . . . . . . . . . . . . . 18 |- ((t e. {z e. RR | -uz e. A} /\ u < t) <-> (t e. RR /\ (-ut e. A /\ u < t)))
55	54