Theorem suppsr 5194

Description: A non-empty, bounded set of positive signed reals has a supremum.

Hypothesis

Ref	Expression
suppsr.1	|- B = {w | [<.(w +P. 1P), 1P>.] ~R e. A}

Assertion

Ref	Expression
suppsr	|- (((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)))))))

Distinct variable groups:   x,w,A   x,y,z,B,w

Proof of Theorem suppsr

Step	Hyp	Ref	Expression
1		supexpr 5135	. . . 4 |- (((B (_ P. /\ -. B = (/)) /\ E.w(w e. P. /\ A.v(v e. P. -> (v e. B -> v <P w)))) -> E.w(w e. P. /\ A.v(v e. P. -> ((v e. B -> -. w <P v) /\ (v <P w -> E.u(u e. P. /\ (u e. B /\ v <P u)))))))
2		enrex 5150	. . . . . 6 |- ~R e. V
3		ecexg 4249	. . . . . 6 |- ( ~R e. V -> [<.(w +P. 1P), 1P>.] ~R e. V)
4	2, 3	ax-mp 7	. . . . 5 |- [<.(w +P. 1P), 1P>.] ~R e. V
5		breq1 2612	. . . . . . . . . . 11 |- ([<.(w +P. 1P), 1P>.] ~R = x -> ([<.(w +P. 1P), 1P>.] ~R <R y <-> x <R y))
6	5	negbid 609	. . . . . . . . . 10 |- ([<.(w +P. 1P), 1P>.] ~R = x -> (-. [<.(w +P. 1P), 1P>.] ~R <R y <-> -. x <R y))
7	6	imbi2d 610	. . . . . . . . 9 |- ([<.(w +P. 1P), 1P>.] ~R = x -> ((y e. A -> -. [<.(w +P. 1P), 1P>.] ~R <R y) <-> (y e. A -> -. x <R y)))
8		breq2 2613	. . . . . . . . . 10 |- ([<.(w +P. 1P), 1P>.] ~R = x -> (y <R [<.(w +P. 1P), 1P>.] ~R <-> y <R x))
9	8	imbi1d 611	. . . . . . . . 9 |- ([<.(w +P. 1P), 1P>.] ~R = x -> ((y <R [<.(w +P. 1P), 1P>.] ~R -> E.z(0R <R z /\ (z e. A /\ y <R z))) <-> (y <R x -> E.z(0R <R z /\ (z e. A /\ y <R z)))))
10	7, 9	anbi12d 626	. . . . . . . 8 |- ([<.(w +P. 1P), 1P>.] ~R = x -> (((y e. A -> -. [<.(w +P. 1P), 1P>.] ~R <R y) /\ (y <R [<.(w +P. 1P), 1P>.] ~R -> E.z(0R <R z /\ (z e. A /\ y <R z)))) <-> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(0R <R z /\ (z e. A /\ y <R z))))))
11	10	imbi2d 610	. . . . . . 7 |- ([<.(w +P. 1P), 1P>.] ~R = x -> ((0R <R y -> ((y e. A -> -. [<.(w +P. 1P), 1P>.] ~R <R y) /\ (y <R [<.(w +P. 1P), 1P>.] ~R -> E.z(0R <R z /\ (z e. A /\ y <R z))))) <-> (0R <R y -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(0R <R z /\ (z e. A /\ y <R z)))))))
12	11	albidv 1273	. . . . . 6 |- ([<.(w +P. 1P), 1P>.] ~R = x -> (A.y(0R <R y -> ((y e. A -> -. [<.(w +P. 1P), 1P>.] ~R <R y) /\ (y <R [<.(w +P. 1P), 1P>.] ~R -> E.z(0R <R z /\ (z e. A /\ y <R z))))) <-> 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)))))))
13		ecexg 4249	. . . . . . . 8 |- ( ~R e. V -> [<.(v +P. 1P), 1P>.] ~R e. V)
14	2, 13	ax-mp 7	. . . . . . 7 |- [<.(v +P. 1P), 1P>.] ~R e. V
15		eleq1 1526	. . . . . . . . . 10 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ([<.(v +P. 1P), 1P>.] ~R e. A <-> y e. A))
16		visset 1804	. . . . . . . . . . 11 |- v e. V
17		opreq1 3953	. . . . . . . . . . . . 13 |- (w = v -> (w +P. 1P) = (v +P. 1P))
18		opeq1 2478	. . . . . . . . . . . . 13 |- ((w +P. 1P) = (v +P. 1P) -> <.(w +P. 1P), 1P>. = <.(v +P. 1P), 1P>.)
19		eceq2 4262	. . . . . . . . . . . . 13 |- (<.(w +P. 1P), 1P>. = <.(v +P. 1P), 1P>. -> [<.(w +P. 1P), 1P>.] ~R = [<.(v +P. 1P), 1P>.] ~R )
20	17, 18, 19	3syl 20	. . . . . . . . . . . 12 |- (w = v -> [<.(w +P. 1P), 1P>.] ~R = [<.(v +P. 1P), 1P>.] ~R )
21	20	eleq1d 1532	. . . . . . . . . . 11 |- (w = v -> ([<.(w +P. 1P), 1P>.] ~R e. A <-> [<.(v +P. 1P), 1P>.] ~R e. A))
22		suppsr.1	. . . . . . . . . . 11 |- B = {w | [<.(w +P. 1P), 1P>.] ~R e. A}
23	16, 21, 22	elab2 1892	. . . . . . . . . 10 |- (v e. B <-> [<.(v +P. 1P), 1P>.] ~R e. A)
24	15, 23	syl5bb 530	. . . . . . . . 9 |- ([<.(v +P. 1P), 1P>.] ~R = y -> (v e. B <-> y e. A))
25		breq2 2613	. . . . . . . . . . 11 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ([<.(w +P. 1P), 1P>.] ~R <R [<.(v +P. 1P), 1P>.] ~R <-> [<.(w +P. 1P), 1P>.] ~R <R y))
26		visset 1804	. . . . . . . . . . . 12 |- w e. V
27	26, 16	ltpsrpr 5191	. . . . . . . . . . 11 |- ([<.(w +P. 1P), 1P>.] ~R <R [<.(v +P. 1P), 1P>.] ~R <-> w <P v)
28	25, 27	syl5bbr 532	. . . . . . . . . 10 |- ([<.(v +P. 1P), 1P>.] ~R = y -> (w <P v <-> [<.(w +P. 1P), 1P>.] ~R <R y))
29	28	negbid 609	. . . . . . . . 9 |- ([<.(v +P. 1P), 1P>.] ~R = y -> (-. w <P v <-> -. [<.(w +P. 1P), 1P>.] ~R <R y))
30	24, 29	imbi12d 624	. . . . . . . 8 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ((v e. B -> -. w <P v) <-> (y e. A -> -. [<.(w +P. 1P), 1P>.] ~R <R y)))
31		breq1 2612	. . . . . . . . . 10 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ([<.(v +P. 1P), 1P>.] ~R <R [<.(w +P. 1P), 1P>.] ~R <-> y <R [<.(w +P. 1P), 1P>.] ~R ))
32	16, 26	ltpsrpr 5191	. . . . . . . . . 10 |- ([<.(v +P. 1P), 1P>.] ~R <R [<.(w +P. 1P), 1P>.] ~R <-> v <P w)
33	31, 32	syl5bbr 532	. . . . . . . . 9 |- ([<.(v +P. 1P), 1P>.] ~R = y -> (v <P w <-> y <R [<.(w +P. 1P), 1P>.] ~R ))
34		breq1 2612	. . . . . . . . . . . . 13 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ([<.(v +P. 1P), 1P>.] ~R <R z <-> y <R z))
35	34	anbi2d 614	. . . . . . . . . . . 12 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ((z e. A /\ [<.(v +P. 1P), 1P>.] ~R <R z) <-> (z e. A /\ y <R z)))
36	35	anbi2d 614	. . . . . . . . . . 11 |- ([<.(v +P. 1P), 1P>.] ~R = y -> ((0R <R z /\ (z e. A /\ [<.(v +P. 1P), 1P>.] ~R <R z)) <-> (0R <R z /\ (z e. A /\ y <R z))))
37	36	exbidv 1274	. . . . . . . . . 10 |- ([<.(v +P. 1P), 1P>.] ~R = y -> (E.z(0R <R z /\ (z e. A /\ [<.(v +P. 1P), 1P>.] ~R <R z)) <-> E.z(0R <R z /\ (z e. A /\ y <R z))))
38		ecexg 4249	. . . . . . . . . . . 12 |- ( ~R e. V -> [<.(u +P. 1P), 1P>.] ~R e. V)
39	2, 38	ax-mp 7	. . . . . . . . . . 11 |- [<.(u +P. 1P), 1P>.] ~R e. V
40		eleq1 1526	. . . . . . . . . . . . 13 |- ([<.(u +P. 1P), 1P>.] ~R = z -> ([<.(u +P. 1P), 1P>.] ~R e. A <-> z e. A))
41		visset 1804	. . . . . . . . . . . . . 14 |- u e. V
42		opreq1 3953	. . . . . . . . . . . . . . . 16 |- (w = u -> (w +P. 1P) = (u +P. 1P))
43		opeq1 2478	. . . . . . . . . . . . . . . 16 |- ((w +P. 1P) = (u +P. 1P) -> <.(w +P. 1P), 1P>. = <.(u +P. 1P), 1P>.)
44		eceq2 4262	. . . . . . . . . . . . . . . 16 |- (<.(w +P. 1P), 1P>. = <.(u +P. 1P), 1P>. -> [<.(w +P. 1P), 1P>.] ~R = [<.(u +P. 1P), 1P>.] ~R )
45	42, 43, 44	3syl 20	. . . . . . . . . . . . . . 15 |- (w = u -> [<.(w +P. 1P), 1P>.] ~R = [<.(u +P. 1P), 1P>.] ~R )
46	45	eleq1d 1532	. . . . . . . . . . . . . 14 |- (w = u -> ([<.(w +P. 1P), 1P>.] ~R e. A <-> [<.(u +P. 1P), 1P>.] ~R e. A))
47	41, 46, 22	elab2 1892	. . . . . . . . . . . . 13 |- (