Theorem isdrs2

Description: Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	drsbn0.b	$$⊢B={\mathrm{Base}}_K$$
	drsdirfi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	isdrs2	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)$$

Proof

Step	Hyp	Ref	Expression
1		drsbn0.b	$$⊢B={\mathrm{Base}}_K$$
2		drsdirfi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		drsprs	$$⊢K\in \mathrm{Dirset}\to K\in \mathrm{Proset}$$
4		simpl	$$⊢\left(K\in \mathrm{Dirset}\wedge x\in \left(𝒫B\cap \mathrm{Fin}\right)\right)\to K\in \mathrm{Dirset}$$
5		elinel1	$$⊢x\in \left(𝒫B\cap \mathrm{Fin}\right)\to x\in 𝒫B$$
6	5	elpwid	$$⊢x\in \left(𝒫B\cap \mathrm{Fin}\right)\to x\subseteq B$$
7	6	adantl	$$⊢\left(K\in \mathrm{Dirset}\wedge x\in \left(𝒫B\cap \mathrm{Fin}\right)\right)\to x\subseteq B$$
8		elinel2	$$⊢x\in \left(𝒫B\cap \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
9	8	adantl	$$⊢\left(K\in \mathrm{Dirset}\wedge x\in \left(𝒫B\cap \mathrm{Fin}\right)\right)\to x\in \mathrm{Fin}$$
10	1 2	drsdirfi	$$⊢\left(K\in \mathrm{Dirset}\wedge x\subseteq B\wedge x\in \mathrm{Fin}\right)\to \exists y\in B\forall z\in xz\underset{\dot{}}{\le }y$$
11	4 7 9 10	syl3anc	$$⊢\left(K\in \mathrm{Dirset}\wedge x\in \left(𝒫B\cap \mathrm{Fin}\right)\right)\to \exists y\in B\forall z\in xz\underset{\dot{}}{\le }y$$
12	11	ralrimiva	$$⊢K\in \mathrm{Dirset}\to \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y$$
13	3 12	jca	$$⊢K\in \mathrm{Dirset}\to \left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)$$
14		simpl	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\to K\in \mathrm{Proset}$$
15		0elpw	$$⊢\varnothing \in 𝒫B$$
16		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
17	15 16	elini	$$⊢\varnothing \in \left(𝒫B\cap \mathrm{Fin}\right)$$
18		raleq	$$⊢x=\varnothing \to \left(\forall z\in xz\underset{\dot{}}{\le }y\leftrightarrow \forall z\in \varnothing z\underset{\dot{}}{\le }y\right)$$
19	18	rexbidv	$$⊢x=\varnothing \to \left(\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\leftrightarrow \exists y\in B\forall z\in \varnothing z\underset{\dot{}}{\le }y\right)$$
20	19	rspcv	$$⊢\varnothing \in \left(𝒫B\cap \mathrm{Fin}\right)\to \left(\forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\to \exists y\in B\forall z\in \varnothing z\underset{\dot{}}{\le }y\right)$$
21	17 20	ax-mp	$$⊢\forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\to \exists y\in B\forall z\in \varnothing z\underset{\dot{}}{\le }y$$
22		rexn0	$$⊢\exists y\in B\forall z\in \varnothing z\underset{\dot{}}{\le }y\to B\ne \varnothing$$
23	21 22	syl	$$⊢\forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\to B\ne \varnothing$$
24	23	adantl	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\to B\ne \varnothing$$
25		raleq	$$⊢x=\left\{a,b\right\}\to \left(\forall z\in xz\underset{\dot{}}{\le }y\leftrightarrow \forall z\in \left\{a,b\right\}z\underset{\dot{}}{\le }y\right)$$
26	25	rexbidv	$$⊢x=\left\{a,b\right\}\to \left(\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\leftrightarrow \exists y\in B\forall z\in \left\{a,b\right\}z\underset{\dot{}}{\le }y\right)$$
27		simplr	$$⊢\left(\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\wedge \left(a\in B\wedge b\in B\right)\right)\to \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y$$
28		prelpwi	$$⊢\left(a\in B\wedge b\in B\right)\to \left\{a,b\right\}\in 𝒫B$$
29		prfi	$$⊢\left\{a,b\right\}\in \mathrm{Fin}$$
30	29	a1i	$$⊢\left(a\in B\wedge b\in B\right)\to \left\{a,b\right\}\in \mathrm{Fin}$$
31	28 30	elind	$$⊢\left(a\in B\wedge b\in B\right)\to \left\{a,b\right\}\in \left(𝒫B\cap \mathrm{Fin}\right)$$
32	31	adantl	$$⊢\left(\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\wedge \left(a\in B\wedge b\in B\right)\right)\to \left\{a,b\right\}\in \left(𝒫B\cap \mathrm{Fin}\right)$$
33	26 27 32	rspcdva	$$⊢\left(\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\wedge \left(a\in B\wedge b\in B\right)\right)\to \exists y\in B\forall z\in \left\{a,b\right\}z\underset{\dot{}}{\le }y$$
34		vex	$$⊢a\in \mathrm{V}$$
35		vex	$$⊢b\in \mathrm{V}$$
36		breq1	$$⊢z=a\to \left(z\underset{\dot{}}{\le }y\leftrightarrow a\underset{\dot{}}{\le }y\right)$$
37		breq1	$$⊢z=b\to \left(z\underset{\dot{}}{\le }y\leftrightarrow b\underset{\dot{}}{\le }y\right)$$
38	34 35 36 37	ralpr	$$⊢\forall z\in \left\{a,b\right\}z\underset{\dot{}}{\le }y\leftrightarrow \left(a\underset{\dot{}}{\le }y\wedge b\underset{\dot{}}{\le }y\right)$$
39	38	rexbii	$$⊢\exists y\in B\forall z\in \left\{a,b\right\}z\underset{\dot{}}{\le }y\leftrightarrow \exists y\in B\left(a\underset{\dot{}}{\le }y\wedge b\underset{\dot{}}{\le }y\right)$$
40	33 39	sylib	$$⊢\left(\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\wedge \left(a\in B\wedge b\in B\right)\right)\to \exists y\in B\left(a\underset{\dot{}}{\le }y\wedge b\underset{\dot{}}{\le }y\right)$$
41	40	ralrimivva	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\to \forall a\in B\forall b\in B\exists y\in B\left(a\underset{\dot{}}{\le }y\wedge b\underset{\dot{}}{\le }y\right)$$
42	1 2	isdrs	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge B\ne \varnothing \wedge \forall a\in B\forall b\in B\exists y\in B\left(a\underset{\dot{}}{\le }y\wedge b\underset{\dot{}}{\le }y\right)\right)$$
43	14 24 41 42	syl3anbrc	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)\to K\in \mathrm{Dirset}$$
44	13 43	impbii	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \forall x\in \left(𝒫B\cap \mathrm{Fin}\right)\exists y\in B\forall z\in xz\underset{\dot{}}{\le }y\right)$$