Theorem drsdir

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

	Ref	Expression
Hypotheses	isdrs.b	$$⊢B={\mathrm{Base}}_K$$
	isdrs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	drsdir	$$⊢\left(K\in \mathrm{Dirset}\wedge X\in B\wedge Y\in B\right)\to \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdrs.b	$$⊢B={\mathrm{Base}}_K$$
2		isdrs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3	1 2	isdrs	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\exists z\in B\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\right)$$
4	3	simp3bi	$$⊢K\in \mathrm{Dirset}\to \forall x\in B\forall y\in B\exists z\in B\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)$$
5		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }z\right)$$
6	5	anbi1d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\right)$$
7	6	rexbidv	$$⊢x=X\to \left(\exists z\in B\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\right)$$
8		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }z\right)$$
9	8	anbi2d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
10	9	rexbidv	$$⊢y=Y\to \left(\exists z\in B\left(X\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
11	7 10	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\exists z\in B\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\to \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
12	4 11	syl5com	$$⊢K\in \mathrm{Dirset}\to \left(\left(X\in B\wedge Y\in B\right)\to \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
13	12	3impib	$$⊢\left(K\in \mathrm{Dirset}\wedge X\in B\wedge Y\in B\right)\to \exists z\in B\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)$$