HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem pre-axsup 5356
Description: A non-empty, bounded-above set of reals has a supremum. Axiom 25 of 25 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 5572.
Assertion
Ref Expression
pre-axsup |- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <R x) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))
Distinct variable group:   x,y,z,A
Proof of Theorem pre-axsup
StepHypRef Expression
1 ssel 2114 . . . . . . . . . . . . . . . 16 |- (A (_ RR -> (y e. A -> y e. RR))
21imim1d 28 . . . . . . . . . . . . . . 15 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x <R y)) -> (y e. A -> (y e. A -> -. x <R y))))
3 pm2.43 63 . . . . . . . . . . . . . . 15 |- ((y e. A -> (y e. A -> -. x <R y)) -> (y e. A -> -. x <R y))
42, 3syl6 22 . . . . . . . . . . . . . 14 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x <R y)) -> (y e. A -> -. x <R y)))
5419.20dv 1331 . . . . . . . . . . . . 13 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x <R y)) -> A.y(y e. A -> -. x <R y)))
6 df-ral 1696 . . . . . . . . . . . . 13 |- (A.y e. A -. x <R y <-> A.y(y e. A -> -. x <R y))
75, 6syl6ibr 220 . . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x <R y)) -> A.y e. A -. x <R y))
8 pm3.27 330 . . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ (z e. A /\ y <R z)) -> (z e. A /\ y <R z))
9819.22i 1081 . . . . . . . . . . . . . . . . . 18 |- (E.z(z e. RR /\ (z e. A /\ y <R z)) -> E.z(z e. A /\ y <R z))
10 df-rex 1697 . . . . . . . . . . . . . . . . . 18 |- (E.z e. A y <R z <-> E.z(z e. A /\ y <R z))
119, 10sylibr 207 . . . . . . . . . . . . . . . . 17 |- (E.z(z e. RR /\ (z e. A /\ y <R z)) -> E.z e. A y <R z)
1211imim2i 17 . . . . . . . . . . . . . . . 16 |- ((y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))) -> (y <R x -> E.z e. A y <R z))
1312imim2i 17 . . . . . . . . . . . . . . 15 |- ((y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> (y e. RR -> (y <R x -> E.z e. A y <R z)))
141319.20i 1033 . . . . . . . . . . . . . 14 |- (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y(y e. RR -> (y <R x -> E.z e. A y <R z)))
15 df-ral 1696 . . . . . . . . . . . . . 14 |- (A.y e. RR (y <R x -> E.z e. A y <R z) <-> A.y(y e. RR -> (y <R x -> E.z e. A y <R z)))
1614, 15sylibr 207 . . . . . . . . . . . . 13 |- (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y e. RR (y <R x -> E.z e. A y <R z))
1716a1i 8 . . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y e. RR (y <R x -> E.z e. A y <R z)))
187, 17anim12d 569 . . . . . . . . . . 11 |- (A (_ RR -> ((A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) -> (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
19 jcab 609 . . . . . . . . . . . . 13 |- ((y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> ((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
2019albii 1040 . . . . . . . . . . . 12 |- (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))))) <-> A.y((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
21 19.26 1108 . . . . . . . . . . . 12 |- (A.y((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> (A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
2220, 21bitri 180 . . . . . . . . . . 11 |- (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))))) <-> (A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
2318, 22syl5ib 213 . . . . . . . . . 10 |- (A (_ 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))))) -> (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
2423anim2d 572 . . . . . . . . 9 |- (A (_ RR -> ((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)))))) -> (x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))))
252419.22dv 1332 . . . . . . . 8 |- (A (_ RR -> (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)))))) -> E.x(x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))))
26 df-rex 1697 . . . . . . . 8 |- (E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)) <-> E.x(x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
2725, 26syl6ibr 220 . . . . . . 7 |- (A (_ RR -> (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)))))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
2827adantr 398 . . . . . 6 |- ((A (_ RR /\ -. A = (/)) -> (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)))))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
29 opeq1 2541 . . . . . . . . 9 |- (v = w -> <.v, 0R>. = <.w, 0R>.)
3029eleq1d 1587 . . . . . . . 8 |- (v = w -> (<.v, 0R>. e. A <-> <.w, 0R>. e. A))
3130cbvabv 1956 . . . . . . 7 |- {v | <.v, 0R>. e. A} = {w | <.w, 0R>. e. A}
3231supre 5325 . . . . . 6 |- (((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)))))))
3328, 32syl5 21 . . . . 5 |- ((A (_ RR /\ -. A = (/)) -> (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
3433anabsi5 506 . . . 4 |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))
35 df-rex 1697 . . . . 5 |- (E.x e. RR A.y e. A y <R x <-> E.x(x e. RR /\ A.y e. A y <R x))
36 df-ral 1696 . . . . . . . 8 |- (A.