Theorem isdrs

Description: Property of being 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	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)$$

Proof

Step	Hyp	Ref	Expression
1		isdrs.b	$$⊢B={\mathrm{Base}}_K$$
2		isdrs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		fveq2	$$⊢f=K\to {\mathrm{Base}}_f={\mathrm{Base}}_K$$
4	3 1	eqtr4di	$$⊢f=K\to {\mathrm{Base}}_f=B$$
5		fveq2	$$⊢f=K\to {\le }_f={\le }_K$$
6	5 2	eqtr4di	$$⊢f=K\to {\le }_f=\underset{\dot{}}{\le }$$
7	6	sbceq1d	$$⊢f=K\to \left(\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{\le }/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\right)$$
8	4 7	sbceqbid	$$⊢f=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\le }/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\right)$$
9	1	fvexi	$$⊢B\in \mathrm{V}$$
10	2	fvexi	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
11		neeq1	$$⊢b=B\to \left(b\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
12	11	adantr	$$⊢\left(b=B\wedge r=\underset{\dot{}}{\le }\right)\to \left(b\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
13		rexeq	$$⊢b=B\to \left(\exists z\in b\left(xrz\wedge yrz\right)\leftrightarrow \exists z\in B\left(xrz\wedge yrz\right)\right)$$
14	13	raleqbi1dv	$$⊢b=B\to \left(\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\leftrightarrow \forall y\in B\exists z\in B\left(xrz\wedge yrz\right)\right)$$
15	14	raleqbi1dv	$$⊢b=B\to \left(\forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\leftrightarrow \forall x\in B\forall y\in B\exists z\in B\left(xrz\wedge yrz\right)\right)$$
16		breq	$$⊢r=\underset{\dot{}}{\le }\to \left(xrz\leftrightarrow x\underset{\dot{}}{\le }z\right)$$
17		breq	$$⊢r=\underset{\dot{}}{\le }\to \left(yrz\leftrightarrow y\underset{\dot{}}{\le }z\right)$$
18	16 17	anbi12d	$$⊢r=\underset{\dot{}}{\le }\to \left(\left(xrz\wedge yrz\right)\leftrightarrow \left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\right)$$
19	18	rexbidv	$$⊢r=\underset{\dot{}}{\le }\to \left(\exists z\in B\left(xrz\wedge yrz\right)\leftrightarrow \exists z\in B\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\right)$$
20	19	2ralbidv	$$⊢r=\underset{\dot{}}{\le }\to \left(\forall x\in B\forall y\in B\exists z\in B\left(xrz\wedge yrz\right)\leftrightarrow \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)$$
21	15 20	sylan9bb	$$⊢\left(b=B\wedge r=\underset{\dot{}}{\le }\right)\to \left(\forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\leftrightarrow \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)$$
22	12 21	anbi12d	$$⊢\left(b=B\wedge r=\underset{\dot{}}{\le }\right)\to \left(\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\leftrightarrow \left(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)\right)$$
23	9 10 22	sbc2ie	$$⊢\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\le }/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\leftrightarrow \left(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)$$
24	8 23	bitrdi	$$⊢f=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\leftrightarrow \left(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)\right)$$
25		df-drs	$$⊢\mathrm{Dirset}=\left\{f\in \mathrm{Proset}|\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\left(b\ne \varnothing \wedge \forall x\in b\forall y\in b\exists z\in b\left(xrz\wedge yrz\right)\right)\right\}$$
26	24 25	elrab2	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \left(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)\right)$$
27		3anass	$$⊢\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)\leftrightarrow \left(K\in \mathrm{Proset}\wedge \left(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)\right)$$
28	26 27	bitr4i	$$⊢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)$$