Theorem supxrunb1 6036

Description: The supremum of an unbounded-above set of extended reals is plus infinity.

Assertion

Ref	Expression
supxrunb1	|- (A (_ RR* -> (A.x e. RR E.y e. A x <_ y <-> sup(A, RR*, < ) = +oo))

Distinct variable group:   x,y,A

Proof of Theorem supxrunb1

Step	Hyp	Ref	Expression
1		ssel 2053	. . . . . . . 8 |- (A (_ RR* -> (z e. A -> z e. RR*))
2		pnfnltt 5519	. . . . . . . 8 |- (z e. RR* -> -. +oo < z)
3	1, 2	syl6 22	. . . . . . 7 |- (A (_ RR* -> (z e. A -> -. +oo < z))
4	3	r19.21aiv 1705	. . . . . 6 |- (A (_ RR* -> A.z e. A -. +oo < z)
5	4	adantr 389	. . . . 5 |- ((A (_ RR* /\ A.x e. RR E.y e. A x <_ y) -> A.z e. A -. +oo < z)
6		breq1 2612	. . . . . . . . . . . . . . . . 17 |- (x = (z + 1) -> (x <_ y <-> (z + 1) <_ y))
7	6	rexbidv 1656	. . . . . . . . . . . . . . . 16 |- (x = (z + 1) -> (E.y e. A x <_ y <-> E.y e. A (z + 1) <_ y))
8	7	rcla4va 1866	. . . . . . . . . . . . . . 15 |- (((z + 1) e. RR /\ A.x e. RR E.y e. A x <_ y) -> E.y e. A (z + 1) <_ y)
9	8	adantrr 395	. . . . . . . . . . . . . 14 |- (((z + 1) e. RR /\ (A.x e. RR E.y e. A x <_ y /\ A (_ RR*)) -> E.y e. A (z + 1) <_ y)
10	9	ancoms 436	. . . . . . . . . . . . 13 |- (((A.x e. RR E.y e. A x <_ y /\ A (_ RR*) /\ (z + 1) e. RR) -> E.y e. A (z + 1) <_ y)
11		peano2re 5408	. . . . . . . . . . . . 13 |- (z e. RR -> (z + 1) e. RR)
12	10, 11	sylan2 451	. . . . . . . . . . . 12 |- (((A.x e. RR E.y e. A x <_ y /\ A (_ RR*) /\ z e. RR) -> E.y e. A (z + 1) <_ y)
13		ltp1t 5767	. . . . . . . . . . . . . . . . . . 19 |- (z e. RR -> z < (z + 1))
14	13	adantr 389	. . . . . . . . . . . . . . . . . 18 |- ((z e. RR /\ y e. RR*) -> z < (z + 1))
15		xrltletrt 5536	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. RR* /\ (z + 1) e. RR* /\ y e. RR*) -> ((z < (z + 1) /\ (z + 1) <_ y) -> z < y))
16		rexrt 5471	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z + 1) e. RR -> (z + 1) e. RR*)
17	15, 16	syl3an2 858	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. RR* /\ (z + 1) e. RR /\ y e. RR*) -> ((z < (z + 1) /\ (z + 1) <_ y) -> z < y))
18		rexrt 5471	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. RR -> z e. RR*)
19	17, 18	syl3an1 857	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. RR /\ (z + 1) e. RR /\ y e. RR*) -> ((z < (z + 1) /\ (z + 1) <_ y) -> z < y))
20	19	3expa 831	. . . . . . . . . . . . . . . . . . 19 |- (((z e. RR /\ (z + 1) e. RR) /\ y e. RR*) -> ((z < (z + 1) /\ (z + 1) <_ y) -> z < y))
21	11	ancli 296	. . . . . . . . . . . . . . . . . . 19 |- (z e. RR -> (z e. RR /\ (z + 1) e. RR))
22	20, 21	sylan 448	. . . . . . . . . . . . . . . . . 18 |- ((z e. RR /\ y e. RR*) -> ((z < (z + 1) /\ (z + 1) <_ y) -> z < y))
23	14, 22	mpand 699	. . . . . . . . . . . . . . . . 17 |- ((z e. RR /\ y e. RR*) -> ((z + 1) <_ y -> z < y))
24	23	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((y e. RR* /\ z e. RR) -> ((z + 1) <_ y -> z < y))
25		ssel2 2054	. . . . . . . . . . . . . . . 16 |- ((A (_ RR* /\ y e. A) -> y e. RR*)
26	24, 25	sylan 448	. . . . . . . . . . . . . . 15 |- (((A (_ RR* /\ y e. A) /\ z e. RR) -> ((z + 1) <_ y -> z < y))
27	26	an1rs 488	. . . . . . . . . . . . . 14 |- (((A (_ RR* /\ z e. RR) /\ y e. A) -> ((z + 1) <_ y -> z < y))
28	27	r19.22dva 1731	. . . . . . . . . . . . 13 |- ((A (_ RR* /\ z e. RR) -> (E.y e. A (z + 1) <_ y -> E.y e. A z < y))
29	28	adantll 392	. . . . . . . . . . . 12 |- (((A.x e. RR E.y e. A x <_ y /\ A (_ RR*) /\ z e. RR) -> (E.y e. A (z + 1) <_ y -> E.y e. A z < y))
30	12, 29	mpd 26	. . . . . . . . . . 11 |- (((A.x e. RR E.y e. A x <_ y /\ A (_ RR*) /\ z e. RR) -> E.y e. A z < y)
31	30	exp31 376	. . . . . . . . . 10 |- (A.x e. RR E.y e. A x <_ y -> (A (_ RR* -> (z e. RR -> E.y e. A z < y)))
32	31	a1dd 42	. . . . . . . . 9 |- (A.x e. RR E.y e. A x <_ y -> (A (_ RR* -> (z < +oo -> (z e. RR -> E.y e. A z < y))))
33	32	com4r 41	. . . . . . . 8 |- (z e. RR -> (A.x e. RR E.y e. A x <_ y -> (A (_ RR* -> (z < +oo -> E.y e. A z < y))))
34	33	com13 33	. . . . . . 7 |- (A (_ RR* -> (A.x e. RR E.y e. A x <_ y -> (z e. RR -> (z < +oo -> E.y e. A z < y))))
35	34	imp 350	. . . . . 6 |- ((A (_ RR* /\ A.x e. RR E.y e. A x <_ y) -> (z e. RR -> (z < +oo -> E.y e. A z < y)))
36	35	r19.21aiv 1705	. . . . 5 |- ((A (_ RR* /\ A.x e. RR E.y e. A x <_ y) -> A.z e. RR (z < +oo -> E.y e. A z < y))
37	5, 36	jca 288	. . . 4 |- ((A (_ RR* /\ A.x e. RR E.y e. A x <_ y) -> (A.z e. A -. +oo < z /\ A.z e. RR (z < +oo -> E.y e. A z < y)))
38		pnfxr 5465	. . . . 5 |- +oo e. RR*
39		supxr 6028	. . . . 5 |- (((A (_ RR* /\ +oo e. RR*) /\ (A.z e. A -. +oo < z /\ A.z e. RR (z < +oo -> E.y e. A z < y))) -> sup(A, RR*, < ) = +oo)
40	38, 39	mpanl2 705	. . . 4 |- ((A (_ RR* /\ (A.z e. A -. +oo < z /\ A.z e. RR (z < +oo -> E.y e. A z < y))) -> sup(A, RR*, < ) = +oo)
41	37, 40	syldan 467	. . 3 |- ((A (_ RR* /\ A.x e. RR E.y e. A x <_ y) -> sup(A, RR*, < ) = +oo)
42	41	ex 373	. 2 |- (A (_ RR* -> (A.x e. RR E.y e. A x <_ y -> sup(A, RR*, < ) = +oo))
43		xrltso 5527	. . . . . . 7 |- < Or RR*
44	43	suplub 4555	. . . . . 6 |- (E.z e. RR* (A.w e. A -. z < w /\ A.w e. RR* (w < z -> E.y e. A w < y)) -> ((x e. RR* /\ x < sup(A, RR*, < )) -> E.y e. A x < y))
45		xrsupss 6025	. . . . . . 7 |- (A (_ RR* -> E.z e. RR* (A.w e. A -. z < w /\ A.w e. RR* (w < z -> E.y e. A w < y)))
46	45	ad2antrr 404	. . . . . 6 |- (((A (_ RR* /\ x e. RR) /\ sup(A, RR*, < ) = +oo) -> E.z e. RR* (A.w e. A -. z < w /\ A.w e. RR* (w < z -> E.y e. A w < y)))
47		rexrt 5471	. . . . . . . 8 |- (x e. RR -> x e. RR*)
48	47	ad2antlr 405	. . . . . . 7 |- (((A (_ RR* /\ x e. RR) /\ sup(A, RR*, < ) = +oo) -> x e. RR*)
49		breq2 2613	. . . . . . . . . 10 |- (sup(A, RR*, < ) = +oo -> (x < sup(A, RR*, < ) <-> x < +oo))
50		ltpnft 5515	. . . . . . . . . 10 |- (x e. RR -> x < +oo)
51	49, 50	syl5bir 210	. . . . . . . . 9 |- (sup(A, RR*, < ) = +oo -> (x e. RR -> x < sup(A, RR*, < )))
52	51	impcom 351	. . . . . . . 8 |- ((x e. RR /\ sup(A, RR*, < ) = +oo) -> x < sup(A, RR*, < ))
53	52	adantll 392	. . . . . . 7 |- (((A (_ RR* /\ x e. RR) /\ sup(A, RR*, < ) = +oo) -> x < sup(A, RR*, < ))
54	48, 53	jca 288	. . . . . 6 |- (((A (_ RR* /\ x e. RR) /\ sup(A, RR*, < ) = +oo) -> (x e. RR* /\ x < sup(A, RR*, < )))
55	44, 46, 54	sylc 68	. . . . 5 |- (((A (_ RR* /\ x e. RR) /\ sup(A, RR*, < ) = +oo) -> E.y e. A x < y)
56	55	ex 373	. . . 4 |- ((A (_ RR* /\ x e. RR) -> (sup(A, RR*, < ) = +oo -> E.y e. A x < y))
57		xrltlet 5532	. . . . . 6 |- ((x e. RR* /\ y e. RR*) -> (x < y -> x <_ y))
58	47	ad2antlr 405	. . . . . 6 |- (((A (_ RR* /\ x e. RR) /\ y e. A) -> x e. RR*)
59	25	adantlr 393	. . . . . 6 |- (((A (_ RR* /\ x e. RR) /\ y e. A) -> y e. RR*)
60	57, 58, 59	sylanc 471	. . . . 5 |- (((A (_ RR* /\ x e. RR) /\ y e. A) -> (x < y -> x <_ y))
61	60	r19.22dva 1731	. . . 4 |- ((A (_ RR* /\ x e. RR) -> (E.y e. A x < y -> E.y e. A x <_ y))
62	56, 61	syld 27	. . 3 |- ((A (_ RR* /\ x e. RR) -> (sup(A, RR*, < ) = +oo -> E.y e. A x <_ y))
63	62	r19.21adva 1711	. 2 |- (A (_ RR* -> (sup(A, RR*, < ) = +oo -> A.x e. RR E.y e. A x <_