lubl

Description: The LUB of a complete lattice subset is the least 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	lubl	$⊢ (K \in CLat \land S \subseteq B \land X \in B) \to (\forall y \in S y \underset{˙}{\leq} X \to U (S) \underset{˙}{\leq} X)$

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	simprd	$⊢ (K \in CLat \land S \subseteq B) \to \forall z \in B (\forall y \in S y \underset{˙}{\leq} z \to U (S) \underset{˙}{\leq} z)$
6		breq2	$⊢ z = X \to (y \underset{˙}{\leq} z \leftrightarrow y \underset{˙}{\leq} X)$
7	6	ralbidv	$⊢ z = X \to (\forall y \in S y \underset{˙}{\leq} z \leftrightarrow \forall y \in S y \underset{˙}{\leq} X)$
8		breq2	$⊢ z = X \to (U (S) \underset{˙}{\leq} z \leftrightarrow U (S) \underset{˙}{\leq} X)$
9	7 8	imbi12d	$⊢ z = X \to ((\forall y \in S y \underset{˙}{\leq} z \to U (S) \underset{˙}{\leq} z) \leftrightarrow (\forall y \in S y \underset{˙}{\leq} X \to U (S) \underset{˙}{\leq} X))$
10	9	rspccva	$⊢ (\forall z \in B (\forall y \in S y \underset{˙}{\leq} z \to U (S) \underset{˙}{\leq} z) \land X \in B) \to (\forall y \in S y \underset{˙}{\leq} X \to U (S) \underset{˙}{\leq} X)$
11	5 10	stoic3	$⊢ (K \in CLat \land S \subseteq B \land X \in B) \to (\forall y \in S y \underset{˙}{\leq} X \to U (S) \underset{˙}{\leq} X)$

Metamath Proof Explorer