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

Metamath Proof Explorer

Theorem lublem

Description: Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		lublem.b	$⊢ B = {Base}_{K}$
2		lublem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lublem.u	$⊢ U = lub (K)$
4		simpl	$⊢ (K \in CLat \land S \subseteq B) \to K \in CLat$
5	1 3	clatlubcl2	$⊢ (K \in CLat \land S \subseteq B) \to S \in dom U$
6	1 2 3 4 5	lubprop	$⊢ (K \in CLat \land S \subseteq B) \to (\forall y \in S y \underset{˙}{\leq} U (S) \land \forall z \in B (\forall y \in S y \underset{˙}{\leq} z \to U (S) \underset{˙}{\leq} z))$