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

Metamath Proof Explorer

Theorem sup0

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

Ref Expression
Assertion 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 )

Proof

Step Hyp Ref Expression
1 sup0riota 
 |-  ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A A. y e. A -. y R x ) )
2 1 3ad2ant1 
 |-  ( ( 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 ) = ( iota_ x e. A A. y e. A -. y R x ) )
3 simp2r 
 |-  ( ( R Or A /\ ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> A. y e. A -. y R X )
4 simpl 
 |-  ( ( X e. A /\ A. y e. A -. y R X ) -> X e. A )
5 4 anim1i 
 |-  ( ( ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> ( X e. A /\ E! x e. A A. y e. A -. y R x ) )
6 5 3adant1 
 |-  ( ( R Or A /\ ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> ( X e. A /\ E! x e. A A. y e. A -. y R x ) )
7 breq2 
 |-  ( x = X -> ( y R x <-> y R X ) )
8 7 notbid 
 |-  ( x = X -> ( -. y R x <-> -. y R X ) )
9 8 ralbidv 
 |-  ( x = X -> ( A. y e. A -. y R x <-> A. y e. A -. y R X ) )
10 9 riota2 
 |-  ( ( X e. A /\ E! x e. A A. y e. A -. y R x ) -> ( A. y e. A -. y R X <-> ( iota_ x e. A A. y e. A -. y R x ) = X ) )
11 6 10 syl 
 |-  ( ( R Or A /\ ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> ( A. y e. A -. y R X <-> ( iota_ x e. A A. y e. A -. y R x ) = X ) )
12 3 11 mpbid 
 |-  ( ( R Or A /\ ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> ( iota_ x e. A A. y e. A -. y R x ) = X )
13 2 12 eqtrd 
 |-  ( ( 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 )