Theorem infeu

Description: An infimum is unique. (Contributed by AV, 6-Oct-2020)

	Ref	Expression
Hypotheses	infmo.1	|- ( ph -> R Or A )
	infeu.2	|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion	infeu	|- ( ph -> E! x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )

Proof

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