# Metamath Proof Explorer

## Theorem supcl

Description: A supremum belongs to its base class (closure law). See also supub and suplub . (Contributed by NM, 12-Oct-2004)

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 supcl ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in {A}$

### 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 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)$
4 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)$
5 riotacl ${⊢}\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 {A}$
6 4 5 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 {A}$
7 3 6 eqeltrd ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in {A}$