lubub

Description: The LUB of a complete lattice subset is an upper bound. (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	lubub	$⊢ (K \in CLat \land S \subseteq B \land X \in S) \to X \underset{˙}{\leq} U (S)$

Step	Hyp	Ref	Expression
1		lublem.b	$⊢ B = {Base}_{K}$
2		lublem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lublem.u	$⊢ U = lub (K)$
4	1 2 3	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))$
5	4	simpld	$⊢ (K \in CLat \land S \subseteq B) \to \forall y \in S y \underset{˙}{\leq} U (S)$
6		breq1	$⊢ y = X \to (y \underset{˙}{\leq} U (S) \leftrightarrow X \underset{˙}{\leq} U (S))$
7	6	rspccva	$⊢ (\forall y \in S y \underset{˙}{\leq} U (S) \land X \in S) \to X \underset{˙}{\leq} U (S)$
8	5 7	stoic3	$⊢ (K \in CLat \land S \subseteq B \land X \in S) \to X \underset{˙}{\leq} U (S)$

Metamath Proof Explorer