# Metamath Proof Explorer

## Theorem supeu

Description: A supremum is unique. Similar to Theorem I.26 of Apostol p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004)

Ref Expression
Hypotheses supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
supeu.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$
Assertion supeu ${⊢}{\phi }\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
2 supeu.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$
3 1 supmo ${⊢}{\phi }\to {\exists }^{*}{x}\in {A}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$
4 reu5 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)\wedge {\exists }^{*}{x}\in {A}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)\right)$
5 2 3 4 sylanbrc ${⊢}{\phi }\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$