Theorem xrub 6027

Description: By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals.

Assertion

Ref	Expression
xrub	|- ((A (_ RR* /\ B e. RR*) -> (A.x e. RR (x < B -> E.y e. A x < y) <-> A.x e. RR* (x < B -> E.y e. A x < y)))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem xrub

Step	Hyp	Ref	Expression
1		pm2.27 62	. . . . . . . . . 10 |- (x e. RR -> ((x e. RR -> (x < B -> E.y e. A x < y)) -> (x < B -> E.y e. A x < y)))
2	1	a1i 8	. . . . . . . . 9 |- (((A (_ RR* /\ B e. RR*) /\ A.z e. RR (z < B -> E.y e. A z < y)) -> (x e. RR -> ((x e. RR -> (x < B -> E.y e. A x < y)) -> (x < B -> E.y e. A x < y))))
3		breq1 2612	. . . . . . . . . . . . . 14 |- (x = +oo -> (x < B <-> +oo < B))
4	3	negbid 609	. . . . . . . . . . . . 13 |- (x = +oo -> (-. x < B <-> -. +oo < B))
5		pnfnltt 5519	. . . . . . . . . . . . 13 |- (B e. RR* -> -. +oo < B)
6	4, 5	syl5bir 210	. . . . . . . . . . . 12 |- (x = +oo -> (B e. RR* -> -. x < B))
7		pm2.21 76	. . . . . . . . . . . 12 |- (-. x < B -> (x < B -> E.y e. A x < y))
8	6, 7	syl6com 53	. . . . . . . . . . 11 |- (B e. RR* -> (x = +oo -> (x < B -> E.y e. A x < y)))
9	8	ad2antlr 405	. . . . . . . . . 10 |- (((A (_ RR* /\ B e. RR*) /\ A.z e. RR (z < B -> E.y e. A z < y)) -> (x = +oo -> (x < B -> E.y e. A x < y)))
10	9	a1dd 42	. . . . . . . . 9 |- (((A (_ RR* /\ B e. RR*) /\ A.z e. RR (z < B -> E.y e. A z < y)) -> (x = +oo -> ((x e. RR -> (x < B -> E.y e. A x < y)) -> (x < B -> E.y e. A x < y))))
11		breq1 2612	. . . . . . . . . . . 12 |- (x = -oo -> (x < B <-> -oo < B))
12		breq1 2612	. . . . . . . . . . . . 13 |- (x = -oo -> (x < y <-> -oo < y))
13	12	rexbidv 1656	. . . . . . . . . . . 12 |- (x = -oo -> (E.y e. A x < y <-> E.y e. A -oo < y))
14	11, 13	imbi12d 624	. . . . . . . . . . 11 |- (x = -oo -> ((x < B -> E.y e. A x < y) <-> ( -oo < B -> E.y e. A -oo < y)))
15		peano2rem 5414	. . . . . . . . . . . . . . . . . 18 |- (B e. RR -> (B - 1) e. RR)
16		breq1 2612	. . . . . . . . . . . . . . . . . . . 20 |- (z = (B - 1) -> (z < B <-> (B - 1) < B))
17		breq1 2612	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (B - 1) -> (z < y <-> (B - 1) < y))
18	17	rexbidv 1656	. . . . . . . . . . . . . . . . . . . 20 |- (z = (B - 1) -> (E.y e. A z < y <-> E.y e. A (B - 1) < y))
19	16, 18	imbi12d 624	. . . . . . . . . . . . . . . . . . 19 |- (z = (B - 1) -> ((z < B -> E.y e. A z < y) <-> ((B - 1) < B -> E.y e. A (B - 1) < y)))
20	19	rcla4v 1864	. . . . . . . . . . . . . . . . . 18 |- ((B - 1) e. RR -> (A.z e. RR (z < B -> E.y e. A z < y) -> ((B - 1) < B -> E.y e. A (B - 1) < y)))
21	15, 20	syl 10	. . . . . . . . . . . . . . . . 17 |- (B e. RR -> (A.z e. RR (z < B -> E.y e. A z < y) -> ((B - 1) < B -> E.y e. A (B - 1) < y)))
22	21	adantl 388	. . . . . . . . . . . . . . . 16 |- ((A (_ RR* /\ B e. RR) -> (A.z e. RR (z < B -> E.y e. A z < y) -> ((B - 1) < B -> E.y e. A (B - 1) < y)))
23		id 59	. . . . . . . . . . . . . . . . . . 19 |- (((B - 1) < B -> E.y e. A (B - 1) < y) -> ((B - 1) < B -> E.y e. A (B - 1) < y))
24		ltm1t 5771	. . . . . . . . . . . . . . . . . . 19 |- (B e. RR -> (B - 1) < B)
25	23, 24	syl5com 52	. . . . . . . . . . . . . . . . . 18 |- (B e. RR -> (((B - 1) < B -> E.y e. A (B - 1) < y) -> E.y e. A (B - 1) < y))
26	25	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((A (_ RR* /\ B e. RR) -> (((B - 1) < B -> E.y e. A (B - 1) < y) -> E.y e. A (B - 1) < y))
27	15	ad2antlr 405	. . . . . . . . . . . . . . . . . . . 20 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> (B - 1) e. RR)
28		mnfltt 5516	. . . . . . . . . . . . . . . . . . . 20 |- ((B - 1) e. RR -> -oo < (B - 1))
29	27, 28	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> -oo < (B - 1))
30		mnfxr 5466	. . . . . . . . . . . . . . . . . . . . 21 |- -oo e. RR*
31		xrlttrt 5526	. . . . . . . . . . . . . . . . . . . . 21 |- (( -oo e. RR* /\ (B - 1) e. RR* /\ y e. RR*) -> (( -oo < (B - 1) /\ (B - 1) < y) -> -oo < y))
32	30, 31	mp3an1 900	. . . . . . . . . . . . . . . . . . . 20 |- (((B - 1) e. RR* /\ y e. RR*) -> (( -oo < (B - 1) /\ (B - 1) < y) -> -oo < y))
33		rexrt 5471	. . . . . . . . . . . . . . . . . . . . 21 |- ((B - 1) e. RR -> (B - 1) e. RR*)
34	27, 33	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> (B - 1) e. RR*)
35		ssel2 2054	. . . . . . . . . . . . . . . . . . . . 21 |- ((A (_ RR* /\ y e. A) -> y e. RR*)
36	35	adantlr 393	. . . . . . . . . . . . . . . . . . . 20 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> y e. RR*)
37	32, 34, 36	sylanc 471	. . . . . . . . . . . . . . . . . . 19 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> (( -oo < (B - 1) /\ (B - 1) < y) -> -oo < y))
38	29, 37	mpand 699	. . . . . . . . . . . . . . . . . 18 |- (((A (_ RR* /\ B e. RR) /\ y e. A) -> ((B - 1) < y -> -oo < y))
39	38	r19.22dva 1731	. . . . . . . . . . . . . . . . 17 |- ((A (_ RR* /\ B e. RR) -> (E.y e. A (B - 1) < y -> E.y e. A -oo < y))
40	26, 39	syld 27	. . . . . . . . . . . . . . . 16 |- ((A (_ RR* /\ B e. RR) -> (((B - 1) < B -> E.y e. A (B - 1) < y) -> E.y e. A -oo < y))
41	22, 40	syld 27	. . . . . . . . . . . . . . 15 |- ((A (_ RR* /\ B e. RR) -> (A.z e. RR (z < B -> E.y e. A z < y) -> E.y e. A -oo < y))
42	41	a1dd 42	. . . . . . . . . . . . . 14 |- ((A (_ RR* /\ B e. RR) -> (A.z e. RR (z < B -> E.y e. A z < y) -> ( -oo < B -> E.y e. A -oo < y)))
43		id 59	. . . . . . . . . . . . . . . . . 18 |- ((1 < B -> E.y e. A 1 < y) -> (1 < B -> E.y e. A 1 < y))
44		1re 5407	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR
45		ltpnft 5515	. . . . . . . . . . . . . . . . . . . 20 |- (1 e. RR -> 1 < +oo)
46	44, 45	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- 1 < +oo
47		breq2 2613	. . . . . . . . . . . . . . . . . . 19 |- (B = +oo -> (1 < B <-> 1 < +oo))
48	46, 47	mpbiri 194	. . . . . . . . . . . . . . . . . 18 |- (B = +oo -> 1 < B)
49	43, 48	syl5com 52	. . . . . . . . . . . . . . . . 17 |- (B = +oo -> ((1 < B -> E.y e. A 1 < y) -> E.y e. A 1 < y))
50		mnfltt 5516	. . . . . . . . . . . . . . . . . . . . 21 |- (1 e. RR -> -oo < 1)
51	44, 50	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- -oo < 1
52		rexrt 5471	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 e. RR -> 1 e. RR*)
53	44, 52	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR*
54		xrlttrt 5526	. . . . . . . . . . . . . . . . . . . . 21 |- (( -oo e. RR* /\ 1 e. RR* /\ y e. RR*) -> (( -oo < 1 /\ 1 < y) -> -oo < y))
55	30, 53, 54	mp3an12 903	. . . . . . . . . . . . . . . . . . . 20 |- (y e. RR* -> (( -oo < 1 /\ 1 < y) -> -oo < y))
56	51, 55	mpani 696	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR* -> (1 < y -> -oo < y))
57	35, 56	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((A (_ RR* /\ y e. A) -> (1 < y -> -oo < y))
58	57	r19.22dva 1731	. . . . . . . . . . . . . . . . 17 |- (A (_ RR* -> (E.y e. A 1 < y -> E.y e. A -oo < y))
59	49, 58	sylan9r 469	. . . . . . . . . . . . . . . 16 |- ((A (_ RR* /\ B = +oo) -> ((1 < B -> E.y e. A 1 < y) -> E.y e. A -oo < y))
60		breq1 2612	. . . . . . . . . . . . . . . . . . 19 |- (z = 1 -> (z < B <-> 1 < B))
61		breq1 2612	. . . . . . . . . . . . . . . . . . . 20 |- (z = 1 -> (z < y <-> 1 < y))
62	61	rexbidv 1656	. . . . . . . . . . . . . . . . . . 19 |- (z = 1 -> (E.y e. A z < y <-> E.y e. A 1 < y))
63	60, 62	imbi12d 624	. . . . . . . . . . . . . . . . . 18 |- (z = 1 -> ((z < B -> E.y e. A z < y) <-> (1 < B -> E.y e. A 1 < y)))
64	63	rcla4v 1864	. . . . . . . . . . . . . . . . 17 |- (1 e. RR -> (A.z e. RR (z < B -> E.y e. A z < y) -> (1 < B -> E.y e. A 1 < y)))
65	44, 64	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (A.z e. RR (z < B -> E.y e. A z < y) -> (1 < B -> E.y e. A 1 < y))
66	59, 65	syl5 21	. . . . . . . . . . . . . . 15 |- ((A (_ RR* /\ B = +oo) -> (A.z e. RR (z < B -> E.y e. A z < y) -> E.y e. A -oo < y))
67	66	a1dd 42	. . . . . . . . . . . . . 14 |- ((A (_ RR* /\ B = +oo) -> (A.z e. RR (z <