supeu

Description: A supremum is unique. Similar to Theorem I.26 of Apostol p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004)

	Ref	Expression
Hypotheses	supmo.1	$⊢ φ \to R Or A$
	supeu.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
Assertion	supeu	$⊢ φ \to \exists! x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$

Step	Hyp	Ref	Expression
1		supmo.1	$⊢ φ \to R Or A$
2		supeu.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
3	1	supmo	$⊢ φ \to \exists^{*} x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
4		reu5	$⊢ \exists! x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow (\exists x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \land \exists^{*} x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)))$
5	2 3 4	sylanbrc	$⊢ φ \to \exists! x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$

Metamath Proof Explorer