This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supsn

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

Ref Expression
Assertion supsn ⊢ R Or A ∧ B ∈ A → sup B A R = B

Proof

Step Hyp Ref Expression
1 dfsn2 ⊢ B = B B
2 1 supeq1i ⊢ sup B A R = sup B B A R
3 suppr ⊢ R Or A ∧ B ∈ A ∧ B ∈ A → sup B B A R = if B R B B B
4 3 3anidm23 ⊢ R Or A ∧ B ∈ A → sup B B A R = if B R B B B
5 2 4 eqtrid ⊢ R Or A ∧ B ∈ A → sup B A R = if B R B B B
6 ifid ⊢ if B R B B B = B
7 5 6 eqtrdi ⊢ R Or A ∧ B ∈ A → sup B A R = B