glbelss

Description: A member of the domain of the greatest lower bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018)

Step	Hyp	Ref	Expression
1		glbs.b	$⊢ B = {Base}_{K}$
2		glbs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		glbs.g	$⊢ G = glb (K)$
4		glbs.k	$⊢ φ \to K \in V$
5		glbs.s	$⊢ φ \to S \in dom G$
6		biid	$⊢ (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \leftrightarrow (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x))$
7	1 2 3 6 4	glbeldm	$⊢ φ \to (S \in dom G \leftrightarrow (S \subseteq B \land \exists! x \in B (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x))))$
8	5 7	mpbid	$⊢ φ \to (S \subseteq B \land \exists! x \in B (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)))$
9	8	simpld	$⊢ φ \to S \subseteq B$

Metamath Proof Explorer