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	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	posmidm	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\land} X = X$

Step	Hyp	Ref	Expression
1		posjidm.b	$⊢ B = {Base}_{K}$
2		posmidm.m	$⊢ \underset{˙}{\land} = meet (K)$
3		eqid	$⊢ glb (K) = glb (K)$
4		simpl	$⊢ (K \in Poset \land X \in B) \to K \in Poset$
5		simpr	$⊢ (K \in Poset \land X \in B) \to X \in B$
6	3 2 4 5 5	meetval	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\land} X = glb (K) (\{X, X\})$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	1 7	posref	$⊢ (K \in Poset \land X \in B) \to X \leq_{K} X$
9		eqidd	$⊢ (K \in Poset \land X \in B) \to \{X, X\} = \{X, X\}$
10	4 1 5 5 7 8 9 3	glbpr	$⊢ (K \in Poset \land X \in B) \to glb (K) (\{X, X\}) = X$
11	6 10	eqtrd	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\land} X = X$

Metamath Proof Explorer