glbeu

Description: Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbval.b	$⊢ B = {Base}_{K}$
	glbval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	glbval.g	$⊢ G = glb (K)$
	glbval.p	$⊢ ψ \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))$
	glbva.k	$⊢ φ \to K \in V$
	glbval.s	$⊢ φ \to S \in dom G$
Assertion	glbeu	$⊢ φ \to \exists! x \in B ψ$

Step	Hyp	Ref	Expression
1		glbval.b	$⊢ B = {Base}_{K}$
2		glbval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		glbval.g	$⊢ G = glb (K)$
4		glbval.p	$⊢ ψ \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))$
5		glbva.k	$⊢ φ \to K \in V$
6		glbval.s	$⊢ φ \to S \in dom G$
7	1 2 3 4 5	glbeldm	$⊢ φ \to (S \in dom G \leftrightarrow (S \subseteq B \land \exists! x \in B ψ))$
8	6 7	mpbid	$⊢ φ \to (S \subseteq B \land \exists! x \in B ψ)$
9	8	simprd	$⊢ φ \to \exists! x \in B ψ$

Metamath Proof Explorer