# Metamath Proof Explorer

## Theorem supub

Description: A supremum is an upper bound. See also supcl and suplub .

This proof demonstrates how to expand an iota-based definition ( df-iota ) using riotacl2 .

(Contributed by NM, 12-Oct-2004) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
supcl.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 supub ${⊢}{\phi }\to \left({C}\in {B}\to ¬sup\left({B},{A},{R}\right){R}{C}\right)$

### Proof

Step Hyp Ref Expression
1 supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
2 supcl.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 simpl ${⊢}\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)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}$
4 3 a1i ${⊢}{x}\in {A}\to \left(\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)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right)$
5 4 ss2rabi ${⊢}\left\{{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\}\subseteq \left\{{x}\in {A}|\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right\}$
6 1 supval2 ${⊢}{\phi }\to sup\left({B},{A},{R}\right)=\left(\iota {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)$
7 1 2 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)$
8 riotacl2 ${⊢}\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)\to \left(\iota {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)\in \left\{{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\}$
9 7 8 syl ${⊢}{\phi }\to \left(\iota {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)\in \left\{{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\}$
10 6 9 eqeltrd ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in \left\{{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\}$
11 5 10 sseldi ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right\}$
12 breq2 ${⊢}{y}={w}\to \left({x}{R}{y}↔{x}{R}{w}\right)$
13 12 notbid ${⊢}{y}={w}\to \left(¬{x}{R}{y}↔¬{x}{R}{w}\right)$
14 13 cbvralvw ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}↔\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{w}$
15 breq1 ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left({x}{R}{w}↔sup\left({B},{A},{R}\right){R}{w}\right)$
16 15 notbid ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left(¬{x}{R}{w}↔¬sup\left({B},{A},{R}\right){R}{w}\right)$
17 16 ralbidv ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left(\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{w}↔\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}\right)$
18 14 17 syl5bb ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}↔\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}\right)$
19 18 elrab ${⊢}sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right\}↔\left(sup\left({B},{A},{R}\right)\in {A}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}\right)$
20 19 simprbi ${⊢}sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right\}\to \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}$
21 11 20 syl ${⊢}{\phi }\to \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}$
22 breq2 ${⊢}{w}={C}\to \left(sup\left({B},{A},{R}\right){R}{w}↔sup\left({B},{A},{R}\right){R}{C}\right)$
23 22 notbid ${⊢}{w}={C}\to \left(¬sup\left({B},{A},{R}\right){R}{w}↔¬sup\left({B},{A},{R}\right){R}{C}\right)$
24 23 rspccv ${⊢}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}¬sup\left({B},{A},{R}\right){R}{w}\to \left({C}\in {B}\to ¬sup\left({B},{A},{R}\right){R}{C}\right)$
25 21 24 syl ${⊢}{\phi }\to \left({C}\in {B}\to ¬sup\left({B},{A},{R}\right){R}{C}\right)$