Theorem supsn

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

	Ref	Expression
Assertion	supsn	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → sup ( { 𝐵 } , 𝐴 , 𝑅 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐵 } = { 𝐵 , 𝐵 }
2	1	supeq1i	⊢ sup ( { 𝐵 } , 𝐴 , 𝑅 ) = sup ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 )
3		suppr	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → sup ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
4	3	3anidm23	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → sup ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
5	2 4	eqtrid	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → sup ( { 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
6		ifid	⊢ if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) = 𝐵
7	5 6	eqtrdi	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → sup ( { 𝐵 } , 𝐴 , 𝑅 ) = 𝐵 )