lubel

Description: An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	$⊢ B = {Base}_{K}$
	lublem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lublem.u	$⊢ U = lub (K)$
Assertion	lubel	$⊢ (K \in CLat \land X \in S \land S \subseteq B) \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		clatl	$⊢ K \in CLat \to K \in Lat$
5		ssel	$⊢ S \subseteq B \to (X \in S \to X \in B)$
6	5	impcom	$⊢ (X \in S \land S \subseteq B) \to X \in B$
7	1 3	lubsn	$⊢ (K \in Lat \land X \in B) \to U (\{X\}) = X$
8	4 6 7	syl2an	$⊢ (K \in CLat \land (X \in S \land S \subseteq B)) \to U (\{X\}) = X$
9	8	3impb	$⊢ (K \in CLat \land X \in S \land S \subseteq B) \to U (\{X\}) = X$
10		snssi	$⊢ X \in S \to \{X\} \subseteq S$
11	1 2 3	lubss	$⊢ (K \in CLat \land S \subseteq B \land \{X\} \subseteq S) \to U (\{X\}) \underset{˙}{\leq} U (S)$
12	10 11	syl3an3	$⊢ (K \in CLat \land S \subseteq B \land X \in S) \to U (\{X\}) \underset{˙}{\leq} U (S)$
13	12	3com23	$⊢ (K \in CLat \land X \in S \land S \subseteq B) \to U (\{X\}) \underset{˙}{\leq} U (S)$
14	9 13	eqbrtrrd	$⊢ (K \in CLat \land X \in S \land S \subseteq B) \to X \underset{˙}{\leq} U (S)$

Metamath Proof Explorer