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 e. Dirset -> B =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		drsbn0.b	|- B = ( Base ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3	1 2	isdrs	|- ( K e. Dirset <-> ( K e. Proset /\ B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x ( le ` K ) z /\ y ( le ` K ) z ) ) )
4	3	simp2bi	|- ( K e. Dirset -> B =/= (/) )