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 = ι x A | y 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 = ι x A | y ¬ x R y y A y R x z y R z
3 ral0 y ¬ x R y
4 3 biantrur y A y R x z y R z y ¬ x R y y A y R x z y R z
5 rex0 ¬ z y R z
6 imnot ¬ z y R z y R x z y R z ¬ y R x
7 5 6 ax-mp y R x z y R z ¬ y R x
8 7 ralbii y A y R x z y R z y A ¬ y R x
9 4 8 bitr3i y ¬ x R y y A y R x z y R z y A ¬ y R x
10 9 a1i R Or A y ¬ x R y y A y R x z y R z y A ¬ y R x
11 10 riotabidv R Or A ι x A | y ¬ x R y y A y R x z y R z = ι x A | y A ¬ y R x
12 2 11 eqtrd R Or A sup A R = ι x A | y A ¬ y R x