# Metamath Proof Explorer

## Theorem suplub

Description: A supremum is the least upper bound. See also supcl and supub . (Contributed by NM, 13-Oct-2004) (Revised 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 suplub ${⊢}{\phi }\to \left(\left({C}\in {A}\wedge {C}{R}sup\left({B},{A},{R}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\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 simpr ${⊢}\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 {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)$
4 breq1 ${⊢}{y}={w}\to \left({y}{R}{x}↔{w}{R}{x}\right)$
5 breq1 ${⊢}{y}={w}\to \left({y}{R}{z}↔{w}{R}{z}\right)$
6 5 rexbidv ${⊢}{y}={w}\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)$
7 4 6 imbi12d ${⊢}{y}={w}\to \left(\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)↔\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right)$
8 7 cbvralvw ${⊢}\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)↔\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)$
9 3 8 sylib ${⊢}\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 {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)$
10 9 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 {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right)$
11 10 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 {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right\}$
12 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)$
13 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)$
14 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\}$
15 13 14 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\}$
16 12 15 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\}$
17 11 16 sseldi ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right\}$
18 breq2 ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left({w}{R}{x}↔{w}{R}sup\left({B},{A},{R}\right)\right)$
19 18 imbi1d ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left(\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)↔\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right)$
20 19 ralbidv ${⊢}{x}=sup\left({B},{A},{R}\right)\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)↔\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right)$
21 20 elrab ${⊢}sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right\}↔\left(sup\left({B},{A},{R}\right)\in {A}\wedge \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right)$
22 21 simprbi ${⊢}sup\left({B},{A},{R}\right)\in \left\{{x}\in {A}|\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\right\}\to \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)$
23 17 22 syl ${⊢}{\phi }\to \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)$
24 breq1 ${⊢}{w}={C}\to \left({w}{R}sup\left({B},{A},{R}\right)↔{C}{R}sup\left({B},{A},{R}\right)\right)$
25 breq1 ${⊢}{w}={C}\to \left({w}{R}{z}↔{C}{R}{z}\right)$
26 25 rexbidv ${⊢}{w}={C}\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$
27 24 26 imbi12d ${⊢}{w}={C}\to \left(\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)↔\left({C}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)\right)$
28 27 rspccv ${⊢}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\to \left({C}\in {A}\to \left({C}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)\right)$
29 28 impd ${⊢}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}{R}{z}\right)\to \left(\left({C}\in {A}\wedge {C}{R}sup\left({B},{A},{R}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$
30 23 29 syl ${⊢}{\phi }\to \left(\left({C}\in {A}\wedge {C}{R}sup\left({B},{A},{R}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$