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

Metamath Proof Explorer

Theorem clatglb

Description: Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011)

		Ref	Expression
	Hypotheses	clatglb.b	$⊢ B = {Base}_{K}$
		clatglb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		clatglb.g	$⊢ G = glb (K)$
	Assertion	clatglb	$⊢ (K \in CLat \land S \subseteq B) \to (\forall y \in S G (S) \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} G (S)))$

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	$⊢ B = {Base}_{K}$
2		clatglb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		clatglb.g	$⊢ G = glb (K)$
4		simpl	$⊢ (K \in CLat \land S \subseteq B) \to K \in CLat$
5	1 3	clatglbcl2	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom G$
6	1 2 3 4 5	glbprop	$⊢ (K \in CLat \land S \subseteq B) \to (\forall y \in S G (S) \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} G (S)))$