latleeqm1

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	latleeqm1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$

Proof

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	latref	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\leq} X$
5	4	3adant3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\leq} X$
6	5	biantrurd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y))$
7		simp1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Lat$
8		simp2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \in B$
9		simp3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \in B$
10	1 2 3	latlem12	$⊢ (K \in Lat \land (X \in B \land X \in B \land Y \in B)) \to ((X \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \leftrightarrow X \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
11	7 8 8 9 10	syl13anc	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \leftrightarrow X \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
12	6 11	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
13	1 2 3	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
14	13	biantrurd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\leq} (X \underset{˙}{\land} Y)))$
15	12 14	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\leq} (X \underset{˙}{\land} Y)))$
16		latpos	$⊢ K \in Lat \to K \in Poset$
17	16	3ad2ant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Poset$
18	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
19	1 2	posasymb	$⊢ (K \in Poset \land X \underset{˙}{\land} Y \in B \land X \in B) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \leftrightarrow X \underset{˙}{\land} Y = X)$
20	17 18 8 19	syl3anc	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \leftrightarrow X \underset{˙}{\land} Y = X)$
21	15 20	bitrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$

Metamath Proof Explorer

Theorem latleeqm1

Proof