Theorem supxrre 6030

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 5471	. . . . . . . . . 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 5519	. . . . . . . . . . . . . . . . 17 |- (x e. RR* -> -. +oo < x)
5	4	adantr 389	. . . . . . . . . . . . . . . 16 |- ((x e. RR* /\ y = +oo) -> -. +oo < x)
6		breq1 2612	. . . . . . . . . . . . . . . . . 18 |- (y = +oo -> (y < x <-> +oo < x))
7	6	negbid 609	. . . . . . . . . . . . . . . . 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 2053	. . . . . . . . . . . . . . . . . . . . . 22 |- (A (_ RR -> (z e. A -> z e. RR))
14		mnfltt 5516	. . . . . . . . . . . . . . . . . . . . . 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 1285	. . . . . . . . . . . . . . . . . . 19 |- (A (_ RR -> (E.z z e. A -> E.z(z e. A /\ -oo < z)))
18		ne0 2278	. . . . . . . . . . . . . . . . . . 19 |- (A =/= (/) <-> E.z z e. A)
19		df-rex 1642	. . . . . . . . . . . . . . . . . . 19 |- (E.z e. A -oo < z <-> E.z(z e. A /\ -oo < z))
20	17, 18, 19	3imtr4g 551	. . . . . . . . . . . . . . . . . 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 2612	. . . . . . . . . . . . . . . . 17 |- (y = -oo -> (y < x <-> -oo < x))
25		breq1 2612	. . . . . . . . . . . . . . . . . 18 |- (y = -oo -> (y < z <-> -oo < z))
26	25	rexbidv 1656	. . . . . . . . . . . . . . . . 17 |- (y = -oo -> (E.z e. A y < z <-> E.z e. A -oo < z))
27	24, 26	imbi12d 624	. . . . . . . . . . . . . . . 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 885	. . . . . . . . . . 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 5508	. . . . . . . . . . 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 516	. . . . . . . 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 1657	. . . . . . 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 614	. . . . . 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 1797	. . . . 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 2502	. . . 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 797	. . 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 5470	. . . . 5 |- RR (_ RR*
43		reuuniss 2879	. . . . 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 900	. . . 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 5999	. . . 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 5484	. . . . . . 7 |- < Or RR
47	46	supeu 4552	. . . . . 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