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 )