HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem pre-axsup 5303
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 5519.
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 2066 . . . . . . . . . . . . . . . 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 1291 . . . . . . . . . . . . 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 1652 . . . . . . . . . . . . 13 |- (A.y e. A -. x <R y <-> A.y(y e. A -> -. x <R y))
75, 6syl6ibr 213 . . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x <R y)) -> A.y e. A -. x <R y))
8 pm3.27 323 . . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ (z e. A /\ y <R z)) -> (z e. A /\ y <R z))
9819.22i 1042 . . . . . . . . . . . . . . . . . 18 |- (E.z(z e. RR /\ (z e. A /\ y <R z)) -> E.z(z e. A /\ y <R z))
10 df-rex 1653 . . . . . . . . . . . . . . . . . 18 |- (E.z e. A y <R z <-> E.z(z e. A /\ y <R z))
119, 10sylibr 200 . . . . . . . . . . . . . . . . 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 994 . . . . . . . . . . . . . 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 1652 . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . 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 560 . . . . . . . . . . 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 600 . . . . . . . . . . . . 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 1001 . . . . . . . . . . . 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 1069 . . . . . . . . . . . 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, 21bitr 173 . . . . . . . . . . 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 206 . . . . . . . . . 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 563 . . . . . . . . 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 1292 . . . . . . . 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 1653 . . . . . . . 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 213 . . . . . . 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 391 . . . . . 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 2491 . . . . . . . . 9 |- (v = w -> <.v, 0R>. = <.w, 0R>.)
3029eleq1d 1543 . . . . . . . 8 |- (v = w -> (<.v, 0R>. e. A <-> <.w, 0R>. e. A))
3130cbvabv 1912 . . . . . . 7 |- {v | <.v, 0R>. e. A} = {w | <.w, 0R>. e. A}
3231supre 5272 . . . . . 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 497 . . . 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 1653 . . . . 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 1652 . . . . . . . 8 |- (A.