latleeqm2

Description: "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011)

	Ref	Expression
Hypotheses	latmle.b	$⊢ B = {Base}_{K}$
	latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	latleeqm2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\land} X = X)$

Step	Hyp	Ref	Expression
1		latmle.b	$⊢ B = {Base}_{K}$
2		latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
4	1 2 3	latleeqm1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
5	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
6	5	eqeq1d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y = X \leftrightarrow Y \underset{˙}{\land} X = X)$
7	4 6	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\land} X = X)$

Metamath Proof Explorer