Theorem sup2 4510

Description: A non-empty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent).

Assertion

Ref	Expression
sup2	|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A (y < x \/ y = x)) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))

Distinct variable group(s):   x,y,z,A

Proof of Theorem sup2

Step	Hyp	Ref	Expression
1		ax1re 4064	. . . . . . . . . . . . 13 |- 1 e. RR
2		axaddrcl 4067	. . . . . . . . . . . . 13 |- ((x e. RR /\ 1 e. RR) -> (x + 1) e. RR)
3	1, 2	mpan2 519	. . . . . . . . . . . 12 |- (x e. RR -> (x + 1) e. RR)
4	3	adantr 306	. . . . . . . . . . 11 |- ((x e. RR /\ A.y e. A (y < x \/ y = x)) -> (x + 1) e. RR)
5	4	a1i 7	. . . . . . . . . 10 |- (A (_ RR -> ((x e. RR /\ A.y e. A (y < x \/ y = x)) -> (x + 1) e. RR))
6		ssel 1502	. . . . . . . . . . . . . . . . . 18 |- (A (_ RR -> (y e. A -> y e. RR))
7		axlttrn 4084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. RR /\ x e. RR /\ (x + 1) e. RR) -> ((y < x /\ x < (x + 1)) -> y < (x + 1)))
8	7	3expb 613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. RR /\ (x e. RR /\ (x + 1) e. RR)) -> ((y < x /\ x < (x + 1)) -> y < (x + 1)))
9	3	ancli 244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> (x e. RR /\ (x + 1) e. RR))
10	8, 9	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. RR /\ x e. RR) -> ((y < x /\ x < (x + 1)) -> y < (x + 1)))
11		ltplus1t 4383	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. RR -> x < (x + 1))
12	10, 11	sylan2i 357	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. RR /\ x e. RR) -> ((y < x /\ x e. RR) -> y < (x + 1)))
13	12	exp4b 296	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. RR -> (x e. RR -> (y < x -> (x e. RR -> y < (x + 1)))))
14	13	com34 36	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. RR -> (x e. RR -> (x e. RR -> (y < x -> y < (x + 1)))))
15	14	pm2.43d 59	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. RR -> (x e. RR -> (y < x -> y < (x + 1))))
16	15	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ x e. RR) -> (y < x -> y < (x + 1)))
17		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = x -> (y < (x + 1) <-> x < (x + 1)))
18	17	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . 22 |- (x < (x + 1) -> (y = x -> y < (x + 1)))
19	11, 18	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. RR -> (y = x -> y < (x + 1)))
20	19	adantl 305	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ x e. RR) -> (y = x -> y < (x + 1)))
21	16, 20	jaod 329	. . . . . . . . . . . . . . . . . . 19 |- ((y e. RR /\ x e. RR) -> ((y < x \/ y = x) -> y < (x + 1)))
22	21	exp 291	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> (x e. RR -> ((y < x \/ y = x) -> y < (x + 1))))
23	6, 22	syl6 23	. . . . . . . . . . . . . . . . 17 |- (A (_ RR -> (y e. A -> (x e. RR -> ((y < x \/ y = x) -> y < (x + 1)))))
24	23	com23 32	. . . . . . . . . . . . . . . 16 |- (A (_ RR -> (x e. RR -> (y e. A -> ((y < x \/ y = x) -> y < (x + 1)))))
25	24	imp 277	. . . . . . . . . . . . . . 15 |- ((A (_ RR /\ x e. RR) -> (y e. A -> ((y < x \/ y = x) -> y < (x + 1))))
26	25	a2d 15	. . . . . . . . . . . . . 14 |- ((A (_ RR /\ x e. RR) -> ((y e. A -> (y < x \/ y = x)) -> (y e. A -> y < (x + 1))))
27	26	19.20dv 946	. . . . . . . . . . . . 13 |- ((A (_ RR /\ x e. RR) -> (A.y(y e. A -> (y < x \/ y = x)) -> A.y(y e. A -> y < (x + 1))))
28		df-ral 1205	. . . . . . . . . . . . 13 |- (A.y e. A (y < x \/ y = x) <-> A.y(y e. A -> (y < x \/ y = x)))
29		df-ral 1205	. . . . . . . . . . . . 13 |- (A.y e. A y < (x + 1) <-> A.y(y e. A -> y < (x + 1)))
30	27, 28, 29	3imtr4g 426	. . . . . . . . . . . 12 |- ((A (_ RR /\ x e. RR) -> (A.y e. A (y < x \/ y = x) -> A.y e. A y < (x + 1)))
31	30	exp 291	. . . . . . . . . . 11 |- (A (_ RR -> (x e. RR -> (A.y e. A (y < x \/ y = x) -> A.y e. A y < (x + 1))))
32	31	imp3a 279	. . . . . . . . . 10 |- (A (_ RR -> ((x e. RR /\ A.y e. A (y < x \/ y = x)) -> A.y e. A y < (x + 1)))
33	5, 32	jcad 455	. . . . . . . . 9 |- (A (_ RR -> ((x e. RR /\ A.y e. A (y < x \/ y = x)) -> ((x + 1) e. RR /\ A.y e. A y < (x + 1))))
34		oprex 3018	. . . . . . . . . 10 |- (x + 1) e. V
35		eleq1 1149	. . . . . . . . . . 11 |- (z = (x + 1) -> (z e. RR <-> (x + 1) e. RR))
36		breq2 2066	. . . . . . . . . . . 12 |- (z = (x + 1) -> (y < z <-> y < (x + 1)))
37	36	biraldv 1219	. . . . . . . . . . 11 |- (z = (x + 1) -> (A.y e. A y < z <-> A.y e. A y < (x + 1)))
38	35, 37	anbi12d 476	. . . . . . . . . 10 |- (z = (x + 1) -> ((z e. RR /\ A.y e. A y < z) <-> ((x + 1) e. RR /\ A.y e. A y < (x + 1))))
39	34, 38	cla4ev 1401	. . . . . . . . 9 |- (((x + 1) e. RR /\ A.y e. A y < (x + 1)) -> E.z(z e. RR /\ A.y e. A y < z))
40	33, 39	syl6 23	. . . . . . . 8 |- (A (_ RR -> ((x e. RR /\ A.y e. A (y < x \/ y = x)) -> E.z(z e. RR /\ A.y e. A y < z)))
41	40	19.23adv 954	. . . . . . 7 |- (A (_ RR -> (E.x(x e. RR /\ A.y e. A (y < x \/ y = x)) -> E.z(z e. RR /\ A.y e. A y < z)))
42		eleq1 1149	. . . . . . . . 9 |- (z = x -> (z e. RR <-> x e. RR))
43		breq2 2066	. . . . . . . . . 10 |- (z = x -> (y < z <-> y < x))
44	43	biraldv 1219	. . . . . . . . 9 |- (z = x -> (A.y e. A y < z <-> A.y e. A y < x))
45	42, 44	anbi12d 476	. . . . . . . 8 |- (z = x -> ((z e. RR /\ A.y e. A y < z) <-> (x e. RR /\ A.y e. A y < x)))
46	45	cbvexv 973	. . . . . . 7 |- (E.z(z e. RR /\ A.y e. A y < z) <-> E.x(x e. RR /\ A.y e. A y < x))
47	41, 46	syl6ib 185	. . . . . 6 |- (A (_ RR -> (E.x(x e. RR /\ A.y e. A (y < x \/ y = x)) -> E.x(x e. RR /\ A.y e. A y < x)))
48		df-rex 1206	. . . . . 6 |- (E.x e. RR A.y e. A (y < x \/ y = x) <-> E.x(x e. RR /\ A.y e. A (y < x \/ y = x)))
49		df-rex 1206	. . . . . 6 |- (E.x e. RR A.y e. A y < x <-> E.x(x e. RR /\ A.y e. A y < x))
50	47, 48, 49	3imtr4g 426	. . . . 5 |- (A (_ RR -> (E.x e. RR A.y e. A (y < x \/ y = x) -> E.x e. RR A.y e. A y < x))
51	50	adantr 306	. . . 4 |- ((A (_ RR /\ A =/= (/)) -> (E.x e. RR A.y e. A (y < x \/ y = x) -> E.x e. RR A.y e. A y < x))
52	51	imdistani 340	. . 3 |- (((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A (y < x \/ y = x)) -> ((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A y < x))
53		df-3an 583	. . 3 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A (y < x \/ y = x)) <-> ((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A (y < x \/ y = x)))
54		df-3an 583	. . 3 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y < x) <-> ((A (_ RR /\ A =/= (/)) /\ E.x e. RR A.y e. A y < x))
55	52, 53, 54	3imtr4 192	. 2 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A (y < x \/ y = x)) -> (A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y < x))
56		axsup 4088	. 2 |- ((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)))
57	55, 56	syl 12	1 |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A (y < x \/ y = x)) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195   /\ wa 196   /\ w3a 581  A.wal 672  E.wex 678   = weq 797   = wceq 1091   e. wcel 1092   =/= wne 1190  A.wral 1201  E.wrex 1202   (_ wss 1487  (/)c0 1707   class class class wbr 2054  (class class class)co 3001  RRcr