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 ( 𝐵 , ∅ , 𝑅 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-sup	⊢ sup ( 𝐵 , ∅ , 𝑅 ) = ∪ { 𝑥 ∈ ∅ ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ ∅ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) }
2		rab0	⊢ { 𝑥 ∈ ∅ ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ ∅ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ∅
3	2	unieqi	⊢ ∪ { 𝑥 ∈ ∅ ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ ∅ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ∪ ∅
4		uni0	⊢ ∪ ∅ = ∅
5	1 3 4	3eqtri	⊢ sup ( 𝐵 , ∅ , 𝑅 ) = ∅