Theorem drsdir

Description: Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	isdrs.b	|- B = ( Base ` K )
	isdrs.l	|- .<_ = ( le ` K )
Assertion	drsdir	|- ( ( K e. Dirset /\ X e. B /\ Y e. B ) -> E. z e. B ( X .<_ z /\ Y .<_ z ) )

Proof

Step	Hyp	Ref	Expression
1		isdrs.b	|- B = ( Base ` K )
2		isdrs.l	|- .<_ = ( 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 .<_ z /\ y .<_ z ) ) )
4	3	simp3bi	|- ( K e. Dirset -> A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) )
5		breq1	|- ( x = X -> ( x .<_ z <-> X .<_ z ) )
6	5	anbi1d	|- ( x = X -> ( ( x .<_ z /\ y .<_ z ) <-> ( X .<_ z /\ y .<_ z ) ) )
7	6	rexbidv	|- ( x = X -> ( E. z e. B ( x .<_ z /\ y .<_ z ) <-> E. z e. B ( X .<_ z /\ y .<_ z ) ) )
8		breq1	|- ( y = Y -> ( y .<_ z <-> Y .<_ z ) )
9	8	anbi2d	|- ( y = Y -> ( ( X .<_ z /\ y .<_ z ) <-> ( X .<_ z /\ Y .<_ z ) ) )
10	9	rexbidv	|- ( y = Y -> ( E. z e. B ( X .<_ z /\ y .<_ z ) <-> E. z e. B ( X .<_ z /\ Y .<_ z ) ) )
11	7 10	rspc2v	|- ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) -> E. z e. B ( X .<_ z /\ Y .<_ z ) ) )
12	4 11	syl5com	|- ( K e. Dirset -> ( ( X e. B /\ Y e. B ) -> E. z e. B ( X .<_ z /\ Y .<_ z ) ) )
13	12	3impib	|- ( ( K e. Dirset /\ X e. B /\ Y e. B ) -> E. z e. B ( X .<_ z /\ Y .<_ z ) )