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

Metamath Proof Explorer

Theorem sup0riota

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

Ref Expression
Assertion sup0riota 
|- ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A A. y e. A -. y R x ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( R Or A -> R Or A )
2 1 supval2 
 |-  ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) ) )
3 ral0 
 |-  A. y e. (/) -. x R y
4 3 biantrur 
 |-  ( A. y e. A ( y R x -> E. z e. (/) y R z ) <-> ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) )
5 rex0 
 |-  -. E. z e. (/) y R z
6 imnot 
 |-  ( -. E. z e. (/) y R z -> ( ( y R x -> E. z e. (/) y R z ) <-> -. y R x ) )
7 5 6 ax-mp 
 |-  ( ( y R x -> E. z e. (/) y R z ) <-> -. y R x )
8 7 ralbii 
 |-  ( A. y e. A ( y R x -> E. z e. (/) y R z ) <-> A. y e. A -. y R x )
9 4 8 bitr3i 
 |-  ( ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) <-> A. y e. A -. y R x )
10 9 a1i 
 |-  ( R Or A -> ( ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) <-> A. y e. A -. y R x ) )
11 10 riotabidv 
 |-  ( R Or A -> ( iota_ x e. A ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) ) = ( iota_ x e. A A. y e. A -. y R x ) )
12 2 11 eqtrd 
 |-  ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A A. y e. A -. y R x ) )