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 ) )