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

Metamath Proof Explorer

Theorem posjidm

Description: Poset join is idempotent. latjidm could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024)

Ref Expression
Hypotheses posjidm.b 
|- B = ( Base ` K )
posjidm.j 
|- .\/ = ( join ` K )
Assertion posjidm 
|- ( ( K e. Poset /\ X e. B ) -> ( X .\/ X ) = X )

Proof

Step Hyp Ref Expression
1 posjidm.b 
 |-  B = ( Base ` K )
2 posjidm.j 
 |-  .\/ = ( join ` K )
3 eqid 
 |-  ( lub ` K ) = ( lub ` K )
4 simpl 
 |-  ( ( K e. Poset /\ X e. B ) -> K e. Poset )
5 simpr 
 |-  ( ( K e. Poset /\ X e. B ) -> X e. B )
6 3 2 4 5 5 joinval 
 |-  ( ( K e. Poset /\ X e. B ) -> ( X .\/ X ) = ( ( lub ` K ) ` { X , X } ) )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 1 7 posref 
 |-  ( ( K e. Poset /\ X e. B ) -> X ( le ` K ) X )
9 eqidd 
 |-  ( ( K e. Poset /\ X e. B ) -> { X , X } = { X , X } )
10 4 1 5 5 7 8 9 3 lubpr 
 |-  ( ( K e. Poset /\ X e. B ) -> ( ( lub ` K ) ` { X , X } ) = X )
11 6 10 eqtrd 
 |-  ( ( K e. Poset /\ X e. B ) -> ( X .\/ X ) = X )