Metamath Proof Explorer

Theorem sup3

Description: A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004)

Ref Expression
Assertion sup3 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$

Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq ℝ\to \left({y}\in {A}\to {y}\in ℝ\right)$
2 leloe ${⊢}\left({y}\in ℝ\wedge {x}\in ℝ\right)\to \left({y}\le {x}↔\left({y}<{x}\vee {y}={x}\right)\right)$
3 2 expcom ${⊢}{x}\in ℝ\to \left({y}\in ℝ\to \left({y}\le {x}↔\left({y}<{x}\vee {y}={x}\right)\right)\right)$
4 1 3 syl9 ${⊢}{A}\subseteq ℝ\to \left({x}\in ℝ\to \left({y}\in {A}\to \left({y}\le {x}↔\left({y}<{x}\vee {y}={x}\right)\right)\right)\right)$
5 4 imp31 ${⊢}\left(\left({A}\subseteq ℝ\wedge {x}\in ℝ\right)\wedge {y}\in {A}\right)\to \left({y}\le {x}↔\left({y}<{x}\vee {y}={x}\right)\right)$
6 5 ralbidva ${⊢}\left({A}\subseteq ℝ\wedge {x}\in ℝ\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)$
7 6 rexbidva ${⊢}{A}\subseteq ℝ\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)$
8 7 anbi2d ${⊢}{A}\subseteq ℝ\to \left(\left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)↔\left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)\right)$
9 8 pm5.32i ${⊢}\left({A}\subseteq ℝ\wedge \left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\right)↔\left({A}\subseteq ℝ\wedge \left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)\right)$
10 3anass ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)↔\left({A}\subseteq ℝ\wedge \left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\right)$
11 3anass ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)↔\left({A}\subseteq ℝ\wedge \left({A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)\right)$
12 9 10 11 3bitr4i ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)↔\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)$
13 sup2 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\vee {y}={x}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
14 12 13 sylbi ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$