Theorem 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	|- ( ph -> R Or A )
	supeu.2	|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Assertion	supeu	|- ( ph -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )

Proof

Step	Hyp	Ref	Expression
1		supmo.1	|- ( ph -> R Or A )
2		supeu.2	|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
3	1	supmo	|- ( ph -> E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
4		reu5	|- ( E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) <-> ( E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) /\ E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
5	2 3 4	sylanbrc	|- ( ph -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )