Theorem infempty

Description: The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020)

	Ref	Expression
Assertion	infempty	|- ( ( R Or A /\ ( X e. A /\ A. y e. A -. X R y ) /\ E! x e. A A. y e. A -. x R y ) -> inf ( (/) , A , R ) = X )

Proof

Step	Hyp	Ref	Expression
1		df-inf	|- inf ( (/) , A , R ) = sup ( (/) , A , `' R )
2		cnvso	|- ( R Or A <-> `' R Or A )
3		brcnvg	|- ( ( y e. A /\ X e. A ) -> ( y `' R X <-> X R y ) )
4	3	ancoms	|- ( ( X e. A /\ y e. A ) -> ( y `' R X <-> X R y ) )
5	4	bicomd	|- ( ( X e. A /\ y e. A ) -> ( X R y <-> y `' R X ) )
6	5	notbid	|- ( ( X e. A /\ y e. A ) -> ( -. X R y <-> -. y `' R X ) )
7	6	ralbidva	|- ( X e. A -> ( A. y e. A -. X R y <-> A. y e. A -. y `' R X ) )
8	7	pm5.32i	|- ( ( X e. A /\ A. y e. A -. X R y ) <-> ( X e. A /\ A. y e. A -. y `' R X ) )
9		brcnvg	|- ( ( y e. A /\ x e. A ) -> ( y `' R x <-> x R y ) )
10	9	ancoms	|- ( ( x e. A /\ y e. A ) -> ( y `' R x <-> x R y ) )
11	10	bicomd	|- ( ( x e. A /\ y e. A ) -> ( x R y <-> y `' R x ) )
12	11	notbid	|- ( ( x e. A /\ y e. A ) -> ( -. x R y <-> -. y `' R x ) )
13	12	ralbidva	|- ( x e. A -> ( A. y e. A -. x R y <-> A. y e. A -. y `' R x ) )
14	13	reubiia	|- ( E! x e. A A. y e. A -. x R y <-> E! x e. A A. y e. A -. y `' R x )
15		sup0	|- ( ( `' R Or A /\ ( X e. A /\ A. y e. A -. y `' R X ) /\ E! x e. A A. y e. A -. y `' R x ) -> sup ( (/) , A , `' R ) = X )
16	2 8 14 15	syl3anb	|- ( ( R Or A /\ ( X e. A /\ A. y e. A -. X R y ) /\ E! x e. A A. y e. A -. x R y ) -> sup ( (/) , A , `' R ) = X )
17	1 16	eqtrid	|- ( ( R Or A /\ ( X e. A /\ A. y e. A -. X R y ) /\ E! x e. A A. y e. A -. x R y ) -> inf ( (/) , A , R ) = X )