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 ROrAXAyA¬yRX∃!xAyA¬yRxsupAR=X

Proof

Step Hyp Ref Expression
1 sup0riota ROrAsupAR=ιxA|yA¬yRx
2 1 3ad2ant1 ROrAXAyA¬yRX∃!xAyA¬yRxsupAR=ιxA|yA¬yRx
3 simp2r ROrAXAyA¬yRX∃!xAyA¬yRxyA¬yRX
4 simpl XAyA¬yRXXA
5 4 anim1i XAyA¬yRX∃!xAyA¬yRxXA∃!xAyA¬yRx
6 5 3adant1 ROrAXAyA¬yRX∃!xAyA¬yRxXA∃!xAyA¬yRx
7 breq2 x=XyRxyRX
8 7 notbid x=X¬yRx¬yRX
9 8 ralbidv x=XyA¬yRxyA¬yRX
10 9 riota2 XA∃!xAyA¬yRxyA¬yRXιxA|yA¬yRx=X
11 6 10 syl ROrAXAyA¬yRX∃!xAyA¬yRxyA¬yRXιxA|yA¬yRx=X
12 3 11 mpbid ROrAXAyA¬yRX∃!xAyA¬yRxιxA|yA¬yRx=X
13 2 12 eqtrd ROrAXAyA¬yRX∃!xAyA¬yRxsupAR=X