# Metamath Proof Explorer

## Theorem supsn

Description: The supremum of a singleton. (Contributed by NM, 2-Oct-2007)

Ref Expression
Assertion supsn ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to sup\left(\left\{{B}\right\},{A},{R}\right)={B}$

### Proof

Step Hyp Ref Expression
1 dfsn2 ${⊢}\left\{{B}\right\}=\left\{{B},{B}\right\}$
2 1 supeq1i ${⊢}sup\left(\left\{{B}\right\},{A},{R}\right)=sup\left(\left\{{B},{B}\right\},{A},{R}\right)$
3 suppr ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\wedge {B}\in {A}\right)\to sup\left(\left\{{B},{B}\right\},{A},{R}\right)=if\left({B}{R}{B},{B},{B}\right)$
4 3 3anidm23 ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to sup\left(\left\{{B},{B}\right\},{A},{R}\right)=if\left({B}{R}{B},{B},{B}\right)$
5 2 4 syl5eq ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to sup\left(\left\{{B}\right\},{A},{R}\right)=if\left({B}{R}{B},{B},{B}\right)$
6 ifid ${⊢}if\left({B}{R}{B},{B},{B}\right)={B}$
7 5 6 eqtrdi ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to sup\left(\left\{{B}\right\},{A},{R}\right)={B}$