latleeqj2

Description: "Less than or equal to" in terms of join. ( chlejb2 analog.) (Contributed by NM, 14-Nov-2011)

	Ref	Expression
Hypotheses	latlej.b	$⊢ B = {Base}_{K}$
	latlej.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latlej.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	latleeqj2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\lor} X = Y)$

Step	Hyp	Ref	Expression
1		latlej.b	$⊢ B = {Base}_{K}$
2		latlej.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latlej.j	$⊢ \underset{˙}{\lor} = join (K)$
4	1 2 3	latleeqj1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\lor} Y = Y)$
5	1 3	latjcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$
6	5	eqeq1d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\lor} Y = Y \leftrightarrow Y \underset{˙}{\lor} X = Y)$
7	4 6	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\lor} X = Y)$

Metamath Proof Explorer