Theorem supxrre 6038

Description: The real and extended real suprema match when the real supremum exists.

Assertion

Ref	Expression
supxrre	|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> sup(A, RR*, < ) = sup(A, RR, < ))

Distinct variable group:   x,y,A

Proof of Theorem supxrre

Step	Hyp	Ref	Expression
1		rexrt 5479	. . . . . . . . . 10 |- (y e. RR -> y e. RR*)
2	1	imim1i 16	. . . . . . . . 9 |- ((y e. RR* -> (y < x -> E.z e. A y < z)) -> (y e. RR -> (y < x -> E.z e. A y < z)))
3		pm3.27 323	. . . . . . . . . . . 12 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y e. RR -> (y < x -> E.z e. A y < z)))
4		pnfnltt 5527	. . . . . . . . . . . . . . . . 17 |- (x e. RR* -> -. +oo < x)
5	4	adantr 389	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = +oo) -> -. +oo < x)
6		breq1 2617	. . . . . . . . . . . . . . . . . 18 |- (y = +oo -> (y < x <-> +oo < x))
7	6	negbid 610	. . . . . . . . . . . . . . . . 17 |- (y = +oo -> (-. y < x <-> -. +oo < x))
8	7	adantl 388	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = +oo) -> (-. y < x <-> -. +oo < x))
9	5, 8	mpbird 196	. . . . . . . . . . . . . . 15 |- ((x e. RR* /\ y = +oo) -> -. y < x)
10	9	pm2.21d 78	. . . . . . . . . . . . . 14 |- ((x e. RR* /\ y = +oo) -> (y < x -> E.z e. A y < z))
11	10	ex 373	. . . . . . . . . . . . 13 |- (x e. RR* -> (y = +oo -> (y < x -> E.z e. A y < z)))
12	11	ad2antlr 405	. . . . . . . . . . . 12 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y = +oo -> (y < x -> E.z e. A y < z)))
13		ssel 2059	. . . . . . . . . . . . . . . . . . . . . 22 |- (A (_ RR -> (z e. A -> z e. RR))
14		mnfltt 5524	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. RR -> -oo < z)
15	13, 14	syl6 22	. . . . . . . . . . . . . . . . . . . . 21 |- (A (_ RR -> (z e. A -> -oo < z))
16	15	ancld 298	. . . . . . . . . . . . . . . . . . . 20 |- (A (_ RR -> (z e. A -> (z e. A /\ -oo < z)))
17	16	19.22dv 1288	. . . . . . . . . . . . . . . . . . 19 |- (A (_ RR -> (E.z z e. A -> E.z(z e. A /\ -oo < z)))
18		ne0 2284	. . . . . . . . . . . . . . . . . . 19 |- (A =/= (/) <-> E.z z e. A)
19		df-rex 1647	. . . . . . . . . . . . . . . . . . 19 |- (E.z e. A -oo < z <-> E.z(z e. A /\ -oo < z))
20	17, 18, 19	3imtr4g 552	. . . . . . . . . . . . . . . . . 18 |- (A (_ RR -> (A =/= (/) -> E.z e. A -oo < z))
21	20	imp 350	. . . . . . . . . . . . . . . . 17 |- ((A (_ RR /\ A =/= (/)) -> E.z e. A -oo < z)
22	21	a1d 12	. . . . . . . . . . . . . . . 16 |- ((A (_ RR /\ A =/= (/)) -> ( -oo < x -> E.z e. A -oo < z))
23	22	ad2antrr 404	. . . . . . . . . . . . . . 15 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> ( -oo < x -> E.z e. A -oo < z))
24		breq1 2617	. . . . . . . . . . . . . . . . 17 |- (y = -oo -> (y < x <-> -oo < x))
25		breq1 2617	. . . . . . . . . . . . . . . . . 18 |- (y = -oo -> (y < z <-> -oo < z))
26	25	rexbidv 1661	. . . . . . . . . . . . . . . . 17 |- (y = -oo -> (E.z e. A y < z <-> E.z e. A -oo < z))
27	24, 26	imbi12d 625	. . . . . . . . . . . . . . . 16 |- (y = -oo -> ((y < x -> E.z e. A y < z) <-> ( -oo < x -> E.z e. A -oo < z)))
28	27	adantl 388	. . . . . . . . . . . . . . 15 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> ((y < x -> E.z e. A y < z) <-> ( -oo < x -> E.z e. A -oo < z)))
29	23, 28	mpbird 196	. . . . . . . . . . . . . 14 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ y = -oo) -> (y < x -> E.z e. A y < z))
30	29	ex 373	. . . . . . . . . . . . 13 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (y = -oo -> (y < x -> E.z e. A y < z)))
31	30	adantr 389	. . . . . . . . . . . 12 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y = -oo -> (y < x -> E.z e. A y < z)))
32	3, 12, 31	3jaod 886	. . . . . . . . . . 11 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> ((y e. RR \/ y = +oo \/ y = -oo) -> (y < x -> E.z e. A y < z)))
33		elxr 5516	. . . . . . . . . . 11 |- (y e. RR* <-> (y e. RR \/ y = +oo \/ y = -oo))
34	32, 33	syl5ib 206	. . . . . . . . . 10 |- ((((A (_ RR /\ A =/= (/)) /\ x e. RR*) /\ (y e. RR -> (y < x -> E.z e. A y < z))) -> (y e. RR* -> (y < x -> E.z e. A y < z)))
35	34	ex 373	. . . . . . . . 9 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((y e. RR -> (y < x -> E.z e. A y < z)) -> (y e. RR* -> (y < x -> E.z e. A y < z))))
36	2, 35	impbid2 517	. . . . . . . 8 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((y e. RR* -> (y < x -> E.z e. A y < z)) <-> (y e. RR -> (y < x -> E.z e. A y < z))))
37	36	ralbidv2 1662	. . . . . . 7 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> (A.y e. RR* (y < x -> E.z e. A y < z) <-> A.y e. RR (y < x -> E.z e. A y < z)))
38	37	anbi2d 615	. . . . . 6 |- (((A (_ RR /\ A =/= (/)) /\ x e. RR*) -> ((A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)) <-> (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
39	38	rabbidv 1802	. . . . 5 |- ((A (_ RR /\ A =/= (/)) -> {x e. RR* | (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))} = {x e. RR* | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))})
40	39	unieqd 2507	. . . 4 |- ((A (_ RR /\ A =/= (/)) -> U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))} = U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))})
41	40	3adant3 798	. . 3 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))} = U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))})
42		ressxr 5478	. . . . 5 |- RR (_ RR*
43		reuuniss 2884	. . . . 5 |- ((RR (_ RR* /\ E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) /\ E!x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))) -> U.{x e. RR | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))} = U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))})
44	42, 43	mp3an1 901	. . . 4 |- ((E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) /\ E!x e. RR* (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))) -> U.{x e. RR | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))} = U.{x e. RR* | (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))})
45		sup3 6007	. . . 4 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
46		ltso 5492	. . . . . . 7 |- < Or RR
47	46	supeu 4558	. . . . . 6 |- (E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) -> E!x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
48	45, 47	syl 10	. . . . 5 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> E!x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)