Theorem supsn

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

	Ref	Expression
Assertion	supsn	|- ( ( R Or A /\ B e. 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 e. A /\ B e. A ) -> sup ( { B , B } , A , R ) = if ( B R B , B , B ) )
4	3	3anidm23	|- ( ( R Or A /\ B e. A ) -> sup ( { B , B } , A , R ) = if ( B R B , B , B ) )
5	2 4	eqtrid	|- ( ( R Or A /\ B e. 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 e. A ) -> sup ( { B } , A , R ) = B )