Theorem suppsr2 4017

Description: A non-empty, bounded set of positive signed reals has a supremum. (Converts quantifier restrictions to all reals.)

Assertion

Ref	Expression
suppsr2	|- (((A.x(x e. A -> 0R <R x) /\ -. A = (/)) /\ 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

Proof of Theorem suppsr2

Step	Hyp	Ref	Expression
1		hba1 698	. . . . . 6 |- (A.x(x e. A -> 0R <R x) -> A.xA.x(x e. A -> 0R <R x))
2		ax-17 925	. . . . . 6 |- (-. A = (/) -> A.x -. A = (/))
3	1, 2	hban 704	. . . . 5 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> A.x(A.x(x e. A -> 0R <R x) /\ -. A = (/)))
4		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (x = z -> (x e. A <-> z e. A))
5		breq2 2066	. . . . . . . . . . . . . . . 16 |- (x = z -> (0R <R x <-> 0R <R z))
6	4, 5	imbi12d 474	. . . . . . . . . . . . . . 15 |- (x = z -> ((x e. A -> 0R <R x) <-> (z e. A -> 0R <R z)))
7	6	a4b1 928	. . . . . . . . . . . . . 14 |- (A.x(x e. A -> 0R <R x) -> (z e. A -> 0R <R z))
8		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (y e. R. <-> z e. R.))
9		eleq1 1149	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (y e. A <-> z e. A))
10		breq1 2065	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (y <R x <-> z <R x))
11	9, 10	imbi12d 474	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> ((y e. A -> y <R x) <-> (z e. A -> z <R x)))
12	8, 11	imbi12d 474	. . . . . . . . . . . . . . . . . 18 |- (y = z -> ((y e. R. -> (y e. A -> y <R x)) <-> (z e. R. -> (z e. A -> z <R x))))
13	12	a4b1 928	. . . . . . . . . . . . . . . . 17 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> (z e. R. -> (z e. A -> z <R x)))
14		visset 1350	. . . . . . . . . . . . . . . . . . 19 |- z e. V
15		ltrelsr 3974	. . . . . . . . . . . . . . . . . . 19 |- <R (_ (R. X. R.)
16	14, 15	brel 2459	. . . . . . . . . . . . . . . . . 18 |- (0R <R z -> (0R e. R. /\ z e. R.))
17	16	pm3.27d 262	. . . . . . . . . . . . . . . . 17 |- (0R <R z -> z e. R.)
18	13, 17	syl5 22	. . . . . . . . . . . . . . . 16 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> (0R <R z -> (z e. A -> z <R x)))
19		anc2l 248	. . . . . . . . . . . . . . . 16 |- ((0R <R z -> (z e. A -> z <R x)) -> (0R <R z -> (z e. A -> (0R <R z /\ z <R x))))
20	18, 19	syl 12	. . . . . . . . . . . . . . 15 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> (0R <R z -> (z e. A -> (0R <R z /\ z <R x))))
21		0r 3983	. . . . . . . . . . . . . . . . 17 |- 0R e. R.
22	21	elisseti 1355	. . . . . . . . . . . . . . . 16 |- 0R e. V
23		ltsosr 3997	. . . . . . . . . . . . . . . 16 |- <R Or R.
24		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
25	22, 23, 15, 14, 24	sotri 2630	. . . . . . . . . . . . . . 15 |- ((0R <R z /\ z <R x) -> 0R <R x)
26	20, 25	syl8 25	. . . . . . . . . . . . . 14 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> (0R <R z -> (z e. A -> 0R <R x)))
27	7, 26	sylan9 359	. . . . . . . . . . . . 13 |- ((A.x(x e. A -> 0R <R x) /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (z e. A -> (z e. A -> 0R <R x)))
28	27	pm2.43d 59	. . . . . . . . . . . 12 |- ((A.x(x e. A -> 0R <R x) /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (z e. A -> 0R <R x))
29	28	19.23adv 954	. . . . . . . . . . 11 |- ((A.x(x e. A -> 0R <R x) /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (E.z z e. A -> 0R <R x))
30		n0 1714	. . . . . . . . . . 11 |- (-. A = (/) <-> E.z z e. A)
31	29, 30	syl5ib 181	. . . . . . . . . 10 |- ((A.x(x e. A -> 0R <R x) /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (-. A = (/) -> 0R <R x))
32	31	exp 291	. . . . . . . . 9 |- (A.x(x e. A -> 0R <R x) -> (A.y(y e. R. -> (y e. A -> y <R x)) -> (-. A = (/) -> 0R <R x)))
33	32	com23 32	. . . . . . . 8 |- (A.x(x e. A -> 0R <R x) -> (-. A = (/) -> (A.y(y e. R. -> (y e. A -> y <R x)) -> 0R <R x)))
34	33	imp 277	. . . . . . 7 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> (A.y(y e. R. -> (y e. A -> y <R x)) -> 0R <R x))
35		visset 1350	. . . . . . . . . . . 12 |- y e. V
36	35, 15	brel 2459	. . . . . . . . . . 11 |- (0R <R y -> (0R e. R. /\ y e. R.))
37	36	pm3.27d 262	. . . . . . . . . 10 |- (0R <R y -> y e. R.)
38	37	syl4 19	. . . . . . . . 9 |- ((y e. R. -> (y e. A -> y <R x)) -> (0R <R y -> (y e. A -> y <R x)))
39	38	19.20i 691	. . . . . . . 8 |- (A.y(y e. R. -> (y e. A -> y <R x)) -> A.y(0R <R y -> (y e. A -> y <R x)))
40	39	a1i 7	. . . . . . 7 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> (A.y(y e. R. -> (y e. A -> y <R x)) -> A.y(0R <R y -> (y e. A -> y <R x))))
41	34, 40	jcad 455	. . . . . 6 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> (A.y(y e. R. -> (y e. A -> y <R x)) -> (0R <R x /\ A.y(0R <R y -> (y e. A -> y <R x)))))
42	41	adantld 307	. . . . 5 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> ((x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x))) -> (0R <R x /\ A.y(0R <R y -> (y e. A -> y <R x)))))
43	3, 42	19.22d 744	. . . 4 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> (E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x))) -> E.x(0R <R x /\ A.y(0R <R y -> (y e. A -> y <R x)))))
44	43	imdistani 340	. . 3 |- (((A.x(x e. A -> 0R <R x) /\ -. A = (/)) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x)))) -> ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) /\ E.x(0R <R x /\ A.y(0R <R y -> (y e. A -> y <R x)))))
45		opreq1 3006	. . . . . . 7 |- (v = w -> (v +P. 1P) = (w +P. 1P))
46		opeq1 1876	. . . . . . 7 |- ((v +P. 1P) = (w +P. 1P) -> <.(v +P. 1P), 1P>. = <.(w +P. 1P), 1P>.)
47		eceq2 3215	. . . . . . 7 |- (<.(v +P. 1P), 1P>. = <.(w +P. 1P), 1P>. -> [<.(v +P. 1P), 1P>.] ~R = [<.(w +P. 1P), 1P>.] ~R )
48	45, 46, 47	3syl 21	. . . . . 6 |- (v = w -> [<.(v +P. 1P), 1P>.] ~R = [<.(w +P. 1P), 1P>.] ~R )
49	48	eleq1d 1155	. . . . 5 |- (v = w -> ([<.(v +P. 1P), 1P>.] ~R e. A <-> [<.(w +P. 1P), 1P>.] ~R e. A))
50	49	cbvabv 1424	. . . 4 |- {v | [<.(v +P. 1P), 1P>.] ~R e. A} = {w | [<.(w +P. 1P), 1P>.] ~R e. A}
51	50	suppsr 4016	. . 3 |- (((A.x(x e. A -> 0R <R x) /\ -. A = (/)) /\ E.x(0R <R x /\ A.y(0R <R y -> (y e. A -> y <R x)))) -> E.x(0R <R x /\ A.y(0R <R y -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(0R <R z /\ (z e. A /\ y <R z)))))))
52	44, 51	syl 12	. 2 |- (((A.x(x e. A -> 0R <R x) /\ -. A = (/)) /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x)))) -> E.x(0R <R x /\ A.y(0R <R y -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(0R <R z /\ (z e. A /\ y <R z)))))))
53	24, 15	brel 2459	. . . . . . 7 |- (0R <R x -> (0R e. R. /\ x e. R.))
54	53	pm3.27d 262	. . . . . 6 |- (0R <R x -> x e. R.)
55	54	a1i 7	. . . . 5 |- ((A.x(x e. A -> 0R <R x) /\ -. A = (/)) -> (0R <R x -> x e. R.))
56		eleq1 1149	. . . . . . . . . . . 12 |- (x = y -> (x e. A <-> y e. A))
57		breq2 2066	. . . . . . . . . . . 12 |- (x = y -> (0R <R x <-> 0R <R y))
58	56, 57	imbi12d 474	. . . . . . . . . . 11 |- (x = y -> ((x e. A -> 0R <R x) <-> (y e. A -> 0R <R y)))
59	58	a4b1 928	. . . . . . . . . 10 |- (A.x(x e. A -> 0R <R x) -> (y e. A -> 0R <R y))
60		syl2 17	. . . . . . . . . . 11 |- ((y e. A -> 0R <R y) -> ((0R <R y -> (y e. A -> -. x <R y)) -> (y e. A -> (y e. A -> -. x <R y))