Theorem posmidm

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

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

Proof

Step	Hyp	Ref	Expression
1		posjidm.b	|- B = ( Base ` K )
2		posmidm.m	|- ./\ = ( meet ` K )
3		eqid	|- ( glb ` K ) = ( glb ` 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	meetval	|- ( ( K e. Poset /\ X e. B ) -> ( X ./\ X ) = ( ( glb ` 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	glbpr	|- ( ( K e. Poset /\ X e. B ) -> ( ( glb ` K ) ` { X , X } ) = X )
11	6 10	eqtrd	|- ( ( K e. Poset /\ X e. B ) -> ( X ./\ X ) = X )