This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )