latmle1

Description: A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	latmle.b	$⊢ B = {Base}_{K}$
	latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} 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		simp1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Lat$
5		simp2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \in B$
7		eqid	$⊢ join (K) = join (K)$
8	1 7 3 4 5 6	latcl2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (⟨X, Y⟩ \in dom join (K) \land ⟨X, Y⟩ \in dom \underset{˙}{\land})$
9	8	simprd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
10	1 2 3 4 5 6 9	lemeet1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$

Metamath Proof Explorer