Theorem lubsn

Description: The least upper bound of a singleton. ( chsupsn analog.) (Contributed by NM, 20-Oct-2011)

	Ref	Expression
Hypotheses	lubsn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lubsn.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion	lubsn	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		lubsn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lubsn.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		dfsn2	⊢ { 𝑋 } = { 𝑋 , 𝑋 }
4	3	fveq2i	⊢ ( 𝑈 ‘ { 𝑋 } ) = ( 𝑈 ‘ { 𝑋 , 𝑋 } )
5		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6		simpl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
7		simpr	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8	2 5 6 7 7	joinval	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑋 ) = ( 𝑈 ‘ { 𝑋 , 𝑋 } ) )
9	4 8	eqtr4id	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = ( 𝑋 ( join ‘ 𝐾 ) 𝑋 ) )
10	1 5	latjidm	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑋 ) = 𝑋 )
11	9 10	eqtrd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )