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

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )