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

Metamath Proof Explorer

Theorem clatlubcl

Description: Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	clatlubcl.b	$⊢ B = {Base}_{K}$
	clatlubcl.u	$⊢ U = lub (K)$
Assertion	clatlubcl	$⊢ (K \in CLat \land S \subseteq B) \to U (S) \in B$

Step	Hyp	Ref	Expression
1		clatlubcl.b	$⊢ B = {Base}_{K}$
2		clatlubcl.u	$⊢ U = lub (K)$
3		eqid	$⊢ glb (K) = glb (K)$
4	1 2 3	clatlem	$⊢ (K \in CLat \land S \subseteq B) \to (U (S) \in B \land glb (K) (S) \in B)$
5	4	simpld	$⊢ (K \in CLat \land S \subseteq B) \to U (S) \in B$