This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latmcl

Description: Closure of meet operation in a lattice. ( incom analog.) (Contributed by NM, 14-Sep-2011)

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

Step	Hyp	Ref	Expression
1		latmcl.b	$⊢ B = {Base}_{K}$
2		latmcl.m	$⊢ \underset{˙}{\land} = meet (K)$
3		eqid	$⊢ join (K) = join (K)$
4	1 3 2	latlem	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X join (K) Y \in B \land X \underset{˙}{\land} Y \in B)$
5	4	simprd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$