HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem supre 4054
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 < x)))) -> E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))))
Distinct variable group(s):   x,w,A   x,y,z,B,w
Proof of Theorem supre
StepHypRef Expression
1 supsr 4025 . . . 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 1893 . . . . 5 |- <.w, 0R>. e. V
3 breq1 2065 . . . . . . . . . . 11 |- (<.w, 0R>. = x -> (<.w, 0R>. < y <-> x < y))
43negbid 463 . . . . . . . . . 10 |- (<.w, 0R>. = x -> (-. <.w, 0R>. < y <-> -. x < y))
54imbi2d 464 . . . . . . . . 9 |- (<.w, 0R>. = x -> ((y e. A -> -. <.w, 0R>. < y) <-> (y e. A -> -. x < y)))
6 breq2 2066 . . . . . . . . . 10 |- (<.w, 0R>. = x -> (y < <.w, 0R>. <-> y < x))
76imbi1d 465 . . . . . . . . 9 |- (<.w, 0R>. = x -> ((y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z))) <-> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))
85, 7anbi12d 476 . . . . . . . 8 |- (<.w, 0R>. = x -> (((y e. A -> -. <.w, 0R>. < y) /\ (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z)))) <-> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))))
98imbi2d 464 . . . . . . 7 |- (<.w, 0R>. = x -> ((y e. RR -> ((y e. A -> -. <.w, 0R>. < y) /\ (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> (y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))))
109bialdv 935 . . . . . 6 |- (<.w, 0R>. = x -> (A.y(y e. RR -> ((y e. A -> -. <.w, 0R>. < y) /\ (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))))
11 opex 1893 . . . . . . 7 |- <.v, 0R>. e. V
12 eleq1 1149 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (<.v, 0R>. e. A <-> y e. A))
13 visset 1350 . . . . . . . . . . 11 |- v e. V
14 opeq1 1876 . . . . . . . . . . . 12 |- (w = v -> <.w, 0R>. = <.v, 0R>.)
1514eleq1d 1155 . . . . . . . . . . 11 |- (w = v -> (<.w, 0R>. e. A <-> <.v, 0R>. e. A))
16 supre.1 . . . . . . . . . . 11 |- B = {w | <.w, 0R>. e. A}
1713, 15, 16elab2 1419 . . . . . . . . . 10 |- (v e. B <-> <.v, 0R>. e. A)
1812, 17syl5bb 410 . . . . . . . . 9 |- (<.v, 0R>. = y -> (v e. B <-> y e. A))
19 breq2 2066 . . . . . . . . . . 11 |- (<.v, 0R>. = y -> (<.w, 0R>. < <.v, 0R>. <-> <.w, 0R>. < y))
20 visset 1350 . . . . . . . . . . . 12 |- w e. V
2120, 13ltresr 4052 . . . . . . . . . . 11 |- (<.w, 0R>. < <.v, 0R>. <-> w <R v)
2219, 21syl5bbr 412 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (w <R v <-> <.w, 0R>. < y))
2322negbid 463 . . . . . . . . 9 |- (<.v, 0R>. = y -> (-. w <R v <-> -. <.w, 0R>. < y))
2418, 23imbi12d 474 . . . . . . . 8 |- (<.v, 0R>. = y -> ((v e. B -> -. w <R v) <-> (y e. A -> -. <.w, 0R>. < y)))
25 breq1 2065 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (<.v, 0R>. < <.w, 0R>. <-> y < <.w, 0R>.))
2613, 20ltresr 4052 . . . . . . . . . 10 |- (<.v, 0R>. < <.w, 0R>. <-> v <R w)
2725, 26syl5bbr 412 . . . . . . . . 9 |- (<.v, 0R>. = y -> (v <R w <-> y < <.w, 0R>.))
28 breq1 2065 . . . . . . . . . . . . 13 |- (<.v, 0R>. = y -> (<.v, 0R>. < z <-> y < z))
2928anbi2d 468 . . . . . . . . . . . 12 |- (<.v, 0R>. = y -> ((z e. A /\ <.v, 0R>. < z) <-> (z e. A /\ y < z)))
3029anbi2d 468 . . . . . . . . . . 11 |- (<.v, 0R>. = y -> ((z e. RR /\ (z e. A /\ <.v, 0R>. < z)) <-> (z e. RR /\ (z e. A /\ y < z))))
3130biexdv 936 . . . . . . . . . 10 |- (<.v, 0R>. = y -> (E.z(z e. RR /\ (z e. A /\ <.v, 0R>. < z)) <-> E.z(z e. RR /\ (z e. A /\ y < z))))
32 opex 1893 . . . . . . . . . . 11 |- <.u, 0R>. e. V
33 eleq1 1149 . . . . . . . . . . . . 13 |- (<.u, 0R>. = z -> (<.u, 0R>. e. A <-> z e. A))
34 visset 1350 . . . . . . . . . . . . . 14 |- u e. V
35 opeq1 1876 . . . . . . . . . . . . . . 15 |- (w = u -> <.w, 0R>. = <.u, 0R>.)
3635eleq1d 1155 . . . . . . . . . . . . . 14 |- (w = u -> (<.w, 0R>. e. A <-> <.u, 0R>. e. A))
3734, 36, 16elab2 1419 . . . . . . . . . . . . 13 |- (u e. B <-> <.u, 0R>. e. A)
3833, 37syl5bb 410 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (u e. B <-> z e. A))
39 breq2 2066 . . . . . . . . . . . . 13 |- (<.u, 0R>. = z -> (<.v, 0R>. < <.u, 0R>. <-> <.v, 0R>. < z))
4013, 34ltresr 4052 . . . . . . . . . . . . 13 |- (<.v, 0R>. < <.u, 0R>. <-> v <R u)
4139, 40syl5bbr 412 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (v <R u <-> <.v, 0R>. < z))
4238, 41anbi12d 476 . . . . . . . . . . 11 |- (<.u, 0R>. = z -> ((u e. B /\ v <R u) <-> (z e. A /\ <.v, 0R>. < z)))
43 eleq1 1149 . . . . . . . . . . . 12 |- (<.u, 0R>. = z -> (<.u, 0R>. e. RR <-> z e. RR))
44 opelreal 4043 . . . . . . . . . . . 12 |- (<.u, 0R>. e. RR <-> u e. R.)
4543, 44syl5bbr 412 . . . . . . . . . . 11 |- (<.u, 0R>. = z -> (u e. R. <-> z e. RR))
46 elreal 4044 . . . . . . . . . . 11 |- (z e. RR <-> E.u(u e. R. /\ <.u, 0R>. = z))
4732, 42, 45, 46gencbvex 1372 . . . . . . . . . 10 |- (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. RR /\ (z e. A /\ <.v, 0R>. < z)))
4831, 47syl5bb 410 . . . . . . . . 9 |- (<.v, 0R>. = y -> (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. RR /\ (z e. A /\ y < z))))
4927, 48imbi12d 474 . . . . . . . 8 |- (<.v, 0R>. = y -> ((v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u))) <-> (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z)))))
5024, 49anbi12d 476 . . . . . . 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>. < y) /\ (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z))))))
51 eleq1 1149 . . . . . . . 8 |- (<.v, 0R>. = y -> (<.v, 0R>. e. RR <-> y e. RR))
52 opelreal 4043 . . . . . . . 8 |- (<.v, 0R>. e. RR <-> v e. R.)
5351, 52syl5bbr 412 . . . . . . 7 |- (<.v, 0R>. = y -> (v e. R. <-> y e. RR))
54 elreal 4044 . . . . . . 7 |- (y e. RR <-> E.v(v e. R. /\ <.v, 0R>. = y))
5511, 50, 53, 54gencbval 1373 . . . . . 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>. < y) /\ (y < <.w, 0R>. -> E.z(z e. RR /\ (z e. A /\ y < z))))))
5610, 55syl5bb 410 . . . . 5 |- (<.w, 0R>. = x -> (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 -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))))
57 eleq1 1149 . . . . . 6 |- (<.w, 0R>.