Metamath Proof Explorer

Theorem sup00

Description: The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020)

Ref Expression
Assertion sup00 ⊢ sup B ∅ R = ∅

Proof

Step Hyp Ref Expression
1 df-sup ⊢ sup B ∅ R = ⋃ x ∈ ∅ | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ ∅ y R x → ∃ z ∈ B y R z
2 rab0 ⊢ x ∈ ∅ | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ ∅ y R x → ∃ z ∈ B y R z = ∅
3 2 unieqi ⊢ ⋃ x ∈ ∅ | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ ∅ y R x → ∃ z ∈ B y R z = ⋃ ∅
4 uni0 ⊢ ⋃ ∅ = ∅
5 1 3 4 3eqtri ⊢ sup B ∅ R = ∅