This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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