lubeu

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

	Ref	Expression
Hypotheses	lubval.b	$⊢ B = {Base}_{K}$
	lubval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lubval.u	$⊢ U = lub (K)$
	lubval.p	$⊢ ψ \leftrightarrow (\forall y \in S y \underset{˙}{\leq} x \land \forall z \in B (\forall y \in S y \underset{˙}{\leq} z \to x \underset{˙}{\leq} z))$
	lubval.k	$⊢ φ \to K \in V$
	lubeleu.s	$⊢ φ \to S \in dom U$
Assertion	lubeu	$⊢ φ \to \exists! x \in B ψ$

Step	Hyp	Ref	Expression
1		lubval.b	$⊢ B = {Base}_{K}$
2		lubval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lubval.u	$⊢ U = lub (K)$
4		lubval.p	$⊢ ψ \leftrightarrow (\forall y \in S y \underset{˙}{\leq} x \land \forall z \in B (\forall y \in S y \underset{˙}{\leq} z \to x \underset{˙}{\leq} z))$
5		lubval.k	$⊢ φ \to K \in V$
6		lubeleu.s	$⊢ φ \to S \in dom U$
7	1 2 3 4 5	lubeldm	$⊢ φ \to (S \in dom U \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