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 
|- B = ( Base ` K )
lubsn.u 
|- U = ( lub ` K )
Assertion lubsn 
|- ( ( K e. Lat /\ X e. B ) -> ( U ` { X } ) = X )

Proof

Step Hyp Ref Expression
1 lubsn.b 
 |-  B = ( Base ` K )
2 lubsn.u 
 |-  U = ( lub ` K )
3 dfsn2 
 |-  { X } = { X , X }
4 3 fveq2i 
 |-  ( U ` { X } ) = ( U ` { X , X } )
5 eqid 
 |-  ( join ` K ) = ( join ` K )
6 simpl 
 |-  ( ( K e. Lat /\ X e. B ) -> K e. Lat )
7 simpr 
 |-  ( ( K e. Lat /\ X e. B ) -> X e. B )
8 2 5 6 7 7 joinval 
 |-  ( ( K e. Lat /\ X e. B ) -> ( X ( join ` K ) X ) = ( U ` { X , X } ) )
9 4 8 eqtr4id 
 |-  ( ( K e. Lat /\ X e. B ) -> ( U ` { X } ) = ( X ( join ` K ) X ) )
10 1 5 latjidm 
 |-  ( ( K e. Lat /\ X e. B ) -> ( X ( join ` K ) X ) = X )
11 9 10 eqtrd 
 |-  ( ( K e. Lat /\ X e. B ) -> ( U ` { X } ) = X )