Theorem istos

Description: The predicate "is a toset". (Contributed by FL, 17-Nov-2014)

	Ref	Expression
Hypotheses	istos.b	$$⊢B={\mathrm{Base}}_K$$
	istos.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	istos	$$⊢K\in \mathrm{Toset}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		istos.b	$$⊢B={\mathrm{Base}}_K$$
2		istos.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		fveq2	$$⊢f=K\to {\mathrm{Base}}_f={\mathrm{Base}}_K$$
4		fveq2	$$⊢f=K\to {\le }_f={\le }_K$$
5	4	sbceq1d	$$⊢f=K\to \left(\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \underset{\dot{}}{[}{\le }_K/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right)$$
6	3 5	sbceqbid	$$⊢f=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_K/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_K/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right)$$
7		fvex	$$⊢{\mathrm{Base}}_K\in \mathrm{V}$$
8		fvex	$$⊢{\le }_K\in \mathrm{V}$$
9		eqtr	$$⊢\left(b={\mathrm{Base}}_K\wedge {\mathrm{Base}}_K=B\right)\to b=B$$
10		eqtr	$$⊢\left(r={\le }_K\wedge {\le }_K=\underset{\dot{}}{\le }\right)\to r=\underset{\dot{}}{\le }$$
11		breq	$$⊢r=\underset{\dot{}}{\le }\to \left(xry\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
12		breq	$$⊢r=\underset{\dot{}}{\le }\to \left(yrx\leftrightarrow y\underset{\dot{}}{\le }x\right)$$
13	11 12	orbi12d	$$⊢r=\underset{\dot{}}{\le }\to \left(\left(xry\vee yrx\right)\leftrightarrow \left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
14	13	2ralbidv	$$⊢r=\underset{\dot{}}{\le }\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in b\forall y\in b\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
15		raleq	$$⊢b=B\to \left(\forall y\in b\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
16	15	raleqbi1dv	$$⊢b=B\to \left(\forall x\in b\forall y\in b\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
17	14 16	sylan9bb	$$⊢\left(r=\underset{\dot{}}{\le }\wedge b=B\right)\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
18	17	ex	$$⊢r=\underset{\dot{}}{\le }\to \left(b=B\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)$$
19	10 18	syl	$$⊢\left(r={\le }_K\wedge {\le }_K=\underset{\dot{}}{\le }\right)\to \left(b=B\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)$$
20	19	expcom	$$⊢{\le }_K=\underset{\dot{}}{\le }\to \left(r={\le }_K\to \left(b=B\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)\right)$$
21	20	eqcoms	$$⊢\underset{\dot{}}{\le }={\le }_K\to \left(r={\le }_K\to \left(b=B\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)\right)$$
22	2 21	ax-mp	$$⊢r={\le }_K\to \left(b=B\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)$$
23	9 22	syl5com	$$⊢\left(b={\mathrm{Base}}_K\wedge {\mathrm{Base}}_K=B\right)\to \left(r={\le }_K\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)$$
24	23	expcom	$$⊢{\mathrm{Base}}_K=B\to \left(b={\mathrm{Base}}_K\to \left(r={\le }_K\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)\right)$$
25	24	eqcoms	$$⊢B={\mathrm{Base}}_K\to \left(b={\mathrm{Base}}_K\to \left(r={\le }_K\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)\right)$$
26	1 25	ax-mp	$$⊢b={\mathrm{Base}}_K\to \left(r={\le }_K\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\right)$$
27	26	imp	$$⊢\left(b={\mathrm{Base}}_K\wedge r={\le }_K\right)\to \left(\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
28	7 8 27	sbc2ie	$$⊢\underset{\dot{}}{[}{\mathrm{Base}}_K/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_K/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
29	6 28	bitrdi	$$⊢f=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
30		df-toset	$$⊢\mathrm{Toset}=\left\{f\in \mathrm{Poset}|\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right\}$$
31	29 30	elrab2	$$⊢K\in \mathrm{Toset}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$