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

Step	Hyp	Ref	Expression
1		posjidm.b	$⊢ B = {Base}_{K}$
2		posjidm.j	$⊢ \underset{˙}{\lor} = join (K)$
3		eqid	$⊢ lub (K) = lub (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	joinval	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\lor} X = lub (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	lubpr	$⊢ (K \in Poset \land X \in B) \to lub (K) (\{X, X\}) = X$
11	6 10	eqtrd	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\lor} X = X$

Metamath Proof Explorer