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

Metamath Proof Explorer

Theorem drsbn0

Description: The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypothesis drsbn0.b ⊢ B = Base K
Assertion drsbn0 ⊢ K ∈ Dirset → B ≠ ∅

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢ B = Base K
2 eqid ⊢ ≤ K = ≤ K
3 1 2 isdrs ⊢ K ∈ Dirset ↔ K ∈ Proset ∧ B ≠ ∅ ∧ ∀ x ∈ B ∀ y ∈ B ∃ z ∈ B x ≤ K z ∧ y ≤ K z
4 3 simp2bi ⊢ K ∈ Dirset → B ≠ ∅