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 ⊢ROrA→sup∅AR=ιx∈A|∀y∈A¬yRx

Proof

Step Hyp Ref Expression
1 id ⊢ROrA→ROrA
2 1 supval2 ⊢ROrA→sup∅AR=ιx∈A|∀y∈∅¬xRy∧∀y∈AyRx→∃z∈∅yRz
3 ral0 ⊢∀y∈∅¬xRy
4 3 biantrur ⊢∀y∈AyRx→∃z∈∅yRz↔∀y∈∅¬xRy∧∀y∈AyRx→∃z∈∅yRz
5 rex0 ⊢¬∃z∈∅yRz
6 imnot ⊢¬∃z∈∅yRz→yRx→∃z∈∅yRz↔¬yRx
7 5 6 ax-mp ⊢yRx→∃z∈∅yRz↔¬yRx
8 7 ralbii ⊢∀y∈AyRx→∃z∈∅yRz↔∀y∈A¬yRx
9 4 8 bitr3i ⊢∀y∈∅¬xRy∧∀y∈AyRx→∃z∈∅yRz↔∀y∈A¬yRx
10 9 a1i ⊢ROrA→∀y∈∅¬xRy∧∀y∈AyRx→∃z∈∅yRz↔∀y∈A¬yRx
11 10 riotabidv ⊢ROrA→ιx∈A|∀y∈∅¬xRy∧∀y∈AyRx→∃z∈∅yRz=ιx∈A|∀y∈A¬yRx
12 2 11 eqtrd ⊢ROrA→sup∅AR=ιx∈A|∀y∈A¬yRx