HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem supre 5232
Description: A non-empty, bounded-above set of reals has a supremum.
Hypothesis
Ref Expression
supre.1 |- B = {w | <.w, 0R>. e. A}
Assertion
Ref Expression
supre |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))))
Distinct variable groups:   x,w,A   x,y,z,B,w
Proof of Theorem supre
StepHypRef Expression
1 supsr 5203 . . . 4 |- (((B (_ R. /\ -. B = (/)) /\ E.w(w e. R. /\ A.v(v e. R. -> (v e. B -> v <R w)))) -> E.w(w e. R. /\ A.v(v e. R. -> ((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u)))))))
2 opex 2772 . . . . 5 |- <.w, 0R>. e. V
3 breq1 2612 . . . . . . . . . . 11 |- (<.w, 0R>. = x -> (<.w, 0R>. <R y <-> x <R y))
43negbid 609 . . . . . . . . . 10 |- (<.w, 0R>. = x -> (-. <.w, 0R>. <R y <-> -. x <R y))
54imbi2d 610 . . . . . . . . 9 |- (<.w, 0R>. = x -> ((y e. A -> -. <.w, 0R>. <R y) <-> (y e. A -> -. x <R y)))
6 breq2 2613 . . . . . . . . . 10 |- (<.w, 0R>. = x -> (y <R <.w, 0R>. <-> y <R x))
76imbi1d 611 . . . . . . . . 9 |- (<.w, 0R>. = x -> ((y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z))) <-> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))
85, 7anbi12d 626 . . . . . . . 8 |- (<.w, 0R>. = x -> (((y e. A -> -. <.w, 0R>. <R y) /\ (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z)))) <-> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
98imbi2d 610 . . . . . . 7 |- (<.w, 0R>. = x -> ((y e. RR -> ((y e. A -> -. <.w, 0R>. <R y) /\ (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> (y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))))
109albidv 1273 . . . . . 6 |- (<.w, 0R>. = x -> (A.y(y e. RR -> ((y e. A -> -. <.w, 0R>. <R y) /\ (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))))
11 opex 2772 . . . . . . 7 |- <.v, 0R>. e. V
12 eleq1 1526 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (<.v, 0R>. e. A <-> y e. A))
13 visset 1804 . . . . . . . . . . 11 |- v e. V
14 opeq1 2478 . . . . . . . . . . . 12 |- (w = v -> <.w, 0R>. = <.v, 0R>.)
1514eleq1d 1532 . . . . . . . . . . 11 |- (w = v -> (<.w, 0R>. e. A <-> <.v, 0R>. e. A))
16 supre.1 . . . . . . . . . . 11 |- B = {w | <.w, 0R>. e. A}
1713, 15, 16elab2 1892 . . . . . . . . . 10 |- (v e. B <-> <.v, 0R>. e. A)
1812, 17syl5bb 530 . . . . . . . . 9 |- (<.v, 0R>. = y -> (v e. B <-> y e. A))
19 breq2 2613 . . . . . . . . . . 11 |- (<.v, 0R>. = y -> (<.w, 0R>. <R <.v, 0R>. <-> <.w, 0R>. <R y))
20 visset 1804 . . . . . . . . . . . 12 |- w e. V
2120, 13ltresr 5230 . . . . . . . . . . 11 |- (<.w, 0R>. <R <.v, 0R>. <-> w <R v)
2219, 21syl5bbr 532 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (w <R v <-> <.w, 0R>. <R y))
2322negbid 609 . . . . . . . . 9 |- (<.v, 0R>. = y -> (-. w <R v <-> -. <.w, 0R>. <R y))
2418, 23imbi12d 624 . . . . . . . 8 |- (<.v, 0R>. = y -> ((v e. B -> -. w <R v) <-> (y e. A -> -. <.w, 0R>. <R y)))
25 breq1 2612 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (<.v, 0R>. <R <.w, 0R>. <-> y <R <.w, 0R>.))
2613, 20ltresr 5230 . . . . . . . . . 10 |- (<.v, 0R>. <R <.w, 0R>. <-> v <R w)
2725, 26syl5bbr 532 . . . . . . . . 9 |- (<.v, 0R>. = y -> (v <R w <-> y <R <.w, 0R>.))
28 breq1 2612 . . . . . . . . . . . . 13 |- (<.v, 0R>. = y -> (<.v, 0R>. <R z <-> y <R z))
2928anbi2d 614 . . . . . . . . . . . 12 |- (<.v, 0R>. = y -> ((z e. A /\ <.v, 0R>. <R z) <-> (z e. A /\ y <R z)))
3029anbi2d 614 . . . . . . . . . . 11 |- (<.v, 0R>. = y -> ((z e. RR /\ (z e. A /\ <.v, 0R>. <R z)) <-> (z e. RR /\ (z e. A /\ y <R z))))
3130exbidv 1274 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (E.z(z e. RR /\ (z e. A /\ <.v, 0R>. <R z)) <-> E.z(z e. RR /\ (z e. A /\ y <R z))))
32 opex 2772 . . . . . . . . . . 11 |- <.u, 0R>. e. V
33 eleq1 1526 . . . . . . . . . . . . 13 |- (<.u, 0R>. = z -> (<.u, 0R>. e. A <-> z e. A))
34 visset 1804 . . . . . . . . . . . . . 14 |- u e. V
35 opeq1 2478 . . . . . . . . . . . . . . 15 |- (w = u -> <.w, 0R>. = <.u, 0R>.)
3635eleq1d 1532 . . . . . . . . . . . . . 14 |- (w = u -> (<.w, 0R>. e. A <-> <.u, 0R>. e. A))
3734, 36, 16elab2 1892 . . . . . . . . . . . . 13 |- (u e. B <-> <.u, 0R>. e. A)
3833, 37syl5bb 530 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (u e. B <-> z e. A))
39 breq2 2613 . . . . . . . . . . . . 13 |- (<.u, 0R>. = z -> (<.v, 0R>. <R <.u, 0R>. <-> <.v, 0R>. <R z))
4013, 34ltresr 5230 . . . . . . . . . . . . 13 |- (<.v, 0R>. <R <.u, 0R>. <-> v <R u)
4139, 40syl5bbr 532 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (v <R u <-> <.v, 0R>. <R z))
4238, 41anbi12d 626 . . . . . . . . . . 11 |- (<.u, 0R>. = z -> ((u e. B /\ v <R u) <-> (z e. A /\ <.v, 0R>. <R z)))
43 eleq1 1526 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (<.u, 0R>. e. RR <-> z e. RR))
44 opelreal 5221 . . . . . . . . . . . 12 |- (<.u, 0R>. e. RR <-> u e. R.)
4543, 44syl5bbr 532 . . . . . . . . . . 11 |- (<.u, 0R>. = z -> (u e. R. <-> z e. RR))
46 elreal 5222 . . . . . . . . . . 11 |- (z e. RR <-> E.u(u e. R. /\ <.u, 0R>. = z))
4732, 42, 45, 46gencbvex 1829 . . . . . . . . . 10 |- (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. RR /\ (z e. A /\ <.v, 0R>. <R z)))
4831, 47syl5bb 530 . . . . . . . . 9 |- (<.v, 0R>. = y -> (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. RR /\ (z e. A /\ y <R z))))
4927, 48imbi12d 624 . . . . . . . 8 |- (<.v, 0R>. = y -> ((v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u))) <-> (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z)))))
5024, 49anbi12d 626 . . . . . . 7 |- (<.v, 0R>. = y -> (((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u)))) <-> ((y e. A -> -. <.w, 0R>. <R y) /\ (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
51 eleq1 1526 . . . . . . . 8 |- (<.v, 0R>. = y -> (<.v, 0R>. e. RR <-> y e. RR))
52 opelreal 5221 . . . . . . . 8 |- (<.v, 0R>. e. RR <-> v e. R.)
5351, 52syl5bbr 532 . . . . . . 7 |- (<.v, 0R>. = y -> (v e. R. <-> y e. RR))
54 elreal 5222 . . . . . . 7 |- (y e. RR <-> E.v(v e. R. /\ <.v, 0R>. = y))
5511, 50, 53, 54gencbval 1831 . . . . . 6 |- (A.v(v e. R. -> ((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u))))) <-> A.y(y e. RR -> ((y e. A -> -. <.w, 0R>. <R y) /\ (y <R <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
5610, 55syl5bb 530 . . . . 5 |- (<.w, 0R>. = x -> (A.v(v e. R. -> ((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (