Theorem suppsr3 5196

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 groups:   x,y,z,A   x,B,y,z

Proof of Theorem suppsr3

Step	Hyp	Ref	Expression
1		visset 1804	. . . . . . 7 |- x e. V
2		eleq1 1526	. . . . . . . 8 |- (y = x -> (y e. A <-> x e. A))
3		breq2 2613	. . . . . . . 8 |- (y = x -> (0R <R y <-> 0R <R x))
4	2, 3	anbi12d 626	. . . . . . 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 1892	. . . . . 6 |- (x e. B <-> (x e. A /\ 0R <R x))
7	6	pm3.27bi 326	. . . . 5 |- (x e. B -> 0R <R x)
8	7	ax-gen 960	. . . 4 |- A.x(x e. B -> 0R <R x)
9		suppsr2 5195	. . . 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	mpanl1 704	. . 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 2279	. . . . 5 |- (-. B = (/) <-> E.y y e. B)
12	5	abeq2i 1562	. . . . . 6 |- (y e. B <-> (y e. A /\ 0R <R y))
13	12	exbii 1047	. . . . 5 |- (E.y y e. B <-> E.y(y e. A /\ 0R <R y))
14	11, 13	bitr 173	. . . 4 |- (-. B = (/) <-> E.y(y e. A /\ 0R <R y))
15	14	biimpr 152	. . 3 |- (E.y(y e. A /\ 0R <R y) -> -. B = (/))
16	12	pm3.26bi 322	. . . . . . . 8 |- (y e. B -> y e. A)
17	16	imim1i 16	. . . . . . 7 |- ((y e. A -> y <R x) -> (y e. B -> y <R x))
18	17	imim2i 17	. . . . . 6 |- ((y e. R. -> (y e. A -> y <R x)) -> (y e. R. -> (y e. B -> y <R x)))
19	18	19.20i 989	. . . . 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 335	. . . 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 1036	. . 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 454	. 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 1012	. . . . . . . . 9 |- (E.y(y e. A /\ 0R <R y) -> A.yE.y(y e. A /\ 0R <R y))
24		ax-17 968	. . . . . . . . 9 |- (x e. R. -> A.y x e. R.)
25	23, 24	hban 1006	. . . . . . . 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 1000	. . . . . . . 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 1006	. . . . . . 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 186	. . . . . . . . . . . . . . . . . 18 |- ((y e. B -> -. x <R y) <-> ((y e. A /\ 0R <R y) -> -. x <R y))
29		impexp 347	. . . . . . . . . . . . . . . . . 18 |- (((y e. A /\ 0R <R y) -> -. x <R y) <-> (y e. A -> (0R <R y -> -. x <R y)))
30	28, 29	bitr 173	. . . . . . . . . . . . . . . . 17 |- ((y e. B -> -. x <R y) <-> (y e. A -> (0R <R y -> -. x <R y)))
31		pm2.04 30	. . . . . . . . . . . . . . . . 17 |- ((y e. A -> (0R <R y -> -. x <R y)) -> (0R <R y -> (y e. A -> -. x <R y)))
32	30, 31	sylbi 199	. . . . . . . . . . . . . . . 16 |- ((y e. B -> -. x <R y) -> (0R <R y -> (y e. A -> -. x <R y)))
33	32	imim2i 17	. . . . . . . . . . . . . . 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 981	. . . . . . . . . . . . 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 388	. . . . . . . . . . . 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 1000	. . . . . . . . . . . . . . . . . 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 968	. . . . . . . . . . . . . . . . . 18 |- (0R <R x -> A.y0R <R x)
39	37, 38	hbim 1004	. . . . . . . . . . . . . . . . 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 1004	. . . . . . . . . . . . . . . 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 5175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <R Or R.
42		sotric 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (( <R Or R. /\ (x e. R. /\ y e. R.)) -> (x <R y <-> -. (x = y \/ y <R x)))
43	41, 42	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. R. /\ y e. R.) -> (x <R y <-> -. (x = y \/ y <R x)))
44	43	con2bid 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. R. /\ y e. R.) -> ((x = y \/ y <R x) <-> -. x <R y))
45		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- y e. V
46		ltrelsr 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <R (_ (R. X. R.)
47	45, 46	brel 3213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (0R e. R. /\ y e. R.))
48	47	pm3.27d 325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (0R <R y -> y e. R.)
49	44, 48	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. R. /\ 0R <R y) -> ((x = y \/ y <R x) <-> -. x <R y))
50		breq2 2613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = y -> (0R <R x <-> 0R <R y))
51	50	biimprcd 156	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (x = y -> 0R <R x))
52		0r 5161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- 0R e. R.
53	52	elisseti 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 0R e. V
54	53, 41, 46, 45, 1	sotri 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((0R <R y /\ y <R x) -> 0R <R x)
55	54	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (0R <R y -> (y <R x -> 0R <R x))
56	51, 55	jaod 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (0R <R y -> ((x = y \/ y <R x) -> 0R <R x))
57	56	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. R. /\ 0R <R y) -> ((x = y \/ y <R x) -> 0R <R x))
58	49, 57	sylbird 205	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x e. R. /\ 0R <R y) -> (-. x <R y -> 0R <R x))
59	58	ex 373	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. R. -> (0R <R y -> (-. x <R y ->