Theorem suppsr3 4018

Description: A non-empty, bounded set with at least one positive real has a supremum.

Hypothesis

Ref	Expression
suppsr3.1	|- B = {y | (y e. A /\ 0R <R y)}

Assertion

Ref	Expression
suppsr3	|- ((E.y(y e. A /\ 0R <R y) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x)))) -> E.x(x e. R. /\ A.y(y e. R. -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z)))))))

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

Proof of Theorem suppsr3

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . . 7 |- x e. V
2		eleq1 1149	. . . . . . . 8 |- (y = x -> (y e. A <-> x e. A))
3		breq2 2066	. . . . . . . 8 |- (y = x -> (0R <R y <-> 0R <R x))
4	2, 3	anbi12d 476	. . . . . . 7 |- (y = x -> ((y e. A /\ 0R <R y) <-> (x e. A /\ 0R <R x)))
5		suppsr3.1	. . . . . . 7 |- B = {y | (y e. A /\ 0R <R y)}
6	1, 4, 5	elab2 1419	. . . . . 6 |- (x e. B <-> (x e. A /\ 0R <R x))
7	6	pm3.27bd 263	. . . . 5 |- (x e. B -> 0R <R x)
8	7	ax-gen 677	. . . 4 |- A.x(x e. B -> 0R <R x)
9		suppsr2 4017	. . . 4 |- (((A.x(x e. B -> 0R <R x) /\ -. B = (/)) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. B -> y <R x)))) -> E.x(x e. R. /\ A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z)))))))
10	8, 9	mpan11 529	. . 3 |- ((-. B = (/) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. B -> y <R x)))) -> E.x(x e. R. /\ A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z)))))))
11		n0 1714	. . . . 5 |- (-. B = (/) <-> E.y y e. B)
12	5	cleqabi 1176	. . . . . 6 |- (y e. B <-> (y e. A /\ 0R <R y))
13	12	biex 733	. . . . 5 |- (E.y y e. B <-> E.y(y e. A /\ 0R <R y))
14	11, 13	bitr 151	. . . 4 |- (-. B = (/) <-> E.y(y e. A /\ 0R <R y))
15	14	biimpr 134	. . 3 |- (E.y(y e. A /\ 0R <R y) -> -. B = (/))
16	12	pm3.26bd 259	. . . . . . . 8 |- (y e. B -> y e. A)
17	16	syl4 19	. . . . . . 7 |- ((y e. A -> y <R x) -> (y e. B -> y <R x))
18	17	syl3 18	. . . . . 6 |- ((y e. R. -> (y e. A -> y <R x)) -> (y e. R. -> (y e. B -> y <R x)))
19	18	19.20i 691	. . . . 5 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> A.y(y e. R. -> (y e. B -> y <R x)))
20	19	anim2i 270	. . . 4 |- ((x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (x e. R. /\ A.y(y e. R. -> (y e. B -> y <R x))))
21	20	19.22i 723	. . 3 |- (E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x))) -> E.x(x e. R. /\ A.y(y e. R. -> (y e. B -> y <R x))))
22	10, 15, 21	syl2an 349	. 2 |- ((E.y(y e. A /\ 0R <R y) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x)))) -> E.x(x e. R. /\ A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z)))))))
23		hbe1 709	. . . . . . . . 9 |- (E.y(y e. A /\ 0R <R y) -> A.yE.y(y e. A /\ 0R <R y))
24		ax-17 925	. . . . . . . . 9 |- (x e. R. -> A.y x e. R.)
25	23, 24	hban 704	. . . . . . . 8 |- ((E.y(y e. A /\ 0R <R y) /\ x e. R.) -> A.y(E.y(y e. A /\ 0R <R y) /\ x e. R.))
26		hba1 698	. . . . . . . 8 |- (A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z))))) -> A.yA.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z))))))
27	25, 26	hban 704	. . . . . . 7 |- (((E.y(y e. A /\ 0R <R y) /\ x e. R.) /\ A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z)))))) -> A.y((E.y(y e. A /\ 0R <R y) /\ x e. R.) /\ A.y(y e. R. -> ((y e. B -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. B /\ y <R z)))))))
28	12	imbi1i 161	. . . . . . . . . . . . . . . . . 18 |- ((y e. B -> -. x <R y) <-> ((y e. A /\ 0R <R y) -> -. x <R y))
29		impexp 276	. . . . . . . . . . . . . . . . . 18 |- (((y e. A /\ 0R <R y) -> -. x <R y) <-> (y e. A -> (0R <R y -> -. x <R y)))
30	28, 29	bitr 151	. . . . . . . . . . . . . . . . 17 |- ((y e. B -> -. x <R y) <-> (y e. A -> (0R <R y -> -. x <R y)))
31		pm2.04 31	. . . . . . . . . . . . . . . . 17 |- ((y e. A -> (0R <R y -> -. x <R y)) -> (0R <R y -> (y e. A -> -. x <R y)))
32	30, 31	sylbi 174	. . . . . . . . . . . . . . . 16 |- ((y e. B -> -. x <R y) -> (0R <R y -> (y e. A -> -. x <R y)))
33	32	syl3 18	. . . . . . . . . . . . . . 15 |- ((y e. R. -> (y e. B -> -. x <R y)) -> (y e. R. -> (0R <R y -> (y e. A -> -. x <R y))))
34	33	com23 32	. . . . . . . . . . . . . 14 |- ((y e. R. -> (y e. B -> -. x <R y)) -> (0R <R y -> (y e. R. -> (y e. A -> -. x <R y))))
35	34	a4s 682	. . . . . . . . . . . . 13 |- (A.y(y e. R. -> (y e. B -> -. x <R y)) -> (0R <R y -> (y e. R. -> (y e. A -> -. x <R y))))
36	35	adantl 305	. . . . . . . . . . . 12 |- (((E.y(y e. A /\ 0R <R y) /\ x e. R.) /\ A.y(y e. R. -> (y e. B -> -. x <R y))) -> (0R <R y -> (y e. R. -> (y e. A -> -. x <R y))))
37		hba1 698	. . . . . . . . . . . . . . . . . 18 |- (A.y(y e. R. -> (y e. B -> -. x <R y)) -> A.yA.y(y e. R. -> (y e. B -> -. x <R y)))
38		ax-17 925	. . . . . . . . . . . . . . . . . 18 |- (0R <R x -> A.y0R <R x)
39	37, 38	hbim 702	. . . . . . . . . . . . . . . . 17 |- ((A.y(y e. R. -> (y e. B -> -. x <R y)) -> 0R <R x) -> A.y(A.y(y e. R. -> (y e. B -> -. x <R y)) -> 0R <R x))
40	24, 39	hbim 702	. . . . . . . . . . . . . . . 16 |- ((x e. R. -> (A.y(y e. R. -> (y e. B -> -. x <R y)) -> 0R <R x)) -> A.y(x e. R. -> (A.y(y e. R. -> (y e. B -> -. x <R y)) -> 0R <R x)))
41		ltsosr 3997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <R Or R.
42		sotric 2148	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (( <R Or R. /\ (x e. R. /\ y e. R.)) -> (x <R y <-> -. (x = y \/ y <R x)))
43	41, 42	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. R. /\ y e. R.) -> (x <R y <-> -. (x = y \/ y <R x)))
44	43	bicon2d 404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. R. /\ y e. R.) -> ((x = y \/ y <R x) <-> -. x <R y))
45		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- y e. V
46		ltrelsr 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <R (_ (R. X. R.)
47	45, 46	brel 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (0R e. R. /\ y e. R.))
48	47	pm3.27d 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (0R <R y -> y e. R.)
49	44, 48	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. R. /\ 0R <R y) -> ((x = y \/ y <R x) <-> -. x <R y))
50		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = y -> (0R <R x <-> 0R <R y))
51	50	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (x = y -> 0R <R x))
52		0r 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- 0R e. R.
53	52	elisseti 1355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 0R e. V
54	53, 41, 46, 45, 1	sotri 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((0R <R y /\ y <R x) -> 0R <R x)
55	54	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (y <R x -> 0R <R x))
56	51, 55	jaod 329	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (0R <R y -> ((x = y \/ y <R x) -> 0R <R x))
57	56	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. R. /\ 0R <R y) -> ((x = y \/ y <R x) -> 0R <R x))
58	49, 57	sylbird 180	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x e. R. /\ 0R <R y) -> (-. x <R y -> 0R <R x))
59	58	exp 291	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. R. -> (0R <R y -> (-. x <R y -> 0R <R x)))
60	59	adantld 307	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. R. -> ((y e. A /\ 0R <R y) -> (-. x <R y -> 0R <R x)))
61	60	a2d 15	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. R. -> (((y e. A /\ 0R <R y) -> -. x <R y) -> ((y