Theorem tosso

Description: Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	tosso.b	$$⊢B={\mathrm{Base}}_K$$
	tosso.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	tosso.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	tosso	$$⊢K\in V\to \left(K\in \mathrm{Toset}\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tosso.b	$$⊢B={\mathrm{Base}}_K$$
2		tosso.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		tosso.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4	1 2 3	pleval2	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge y\in B\right)\to \left(x\underset{\dot{}}{\le }y\leftrightarrow \left(x\underset{\dot{}}{<}y\vee x=y\right)\right)$$
5	4	3expb	$$⊢\left(K\in \mathrm{Poset}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\underset{\dot{}}{\le }y\leftrightarrow \left(x\underset{\dot{}}{<}y\vee x=y\right)\right)$$
6	1 2 3	pleval2	$$⊢\left(K\in \mathrm{Poset}\wedge y\in B\wedge x\in B\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow \left(y\underset{\dot{}}{<}x\vee y=x\right)\right)$$
7		equcom	$$⊢y=x\leftrightarrow x=y$$
8	7	orbi2i	$$⊢\left(y\underset{\dot{}}{<}x\vee y=x\right)\leftrightarrow \left(y\underset{\dot{}}{<}x\vee x=y\right)$$
9	6 8	bitrdi	$$⊢\left(K\in \mathrm{Poset}\wedge y\in B\wedge x\in B\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
10	9	3com23	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge y\in B\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
11	10	3expb	$$⊢\left(K\in \mathrm{Poset}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
12	5 11	orbi12d	$$⊢\left(K\in \mathrm{Poset}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)\right)$$
13		df-3or	$$⊢\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee y\underset{\dot{}}{<}x\right)$$
14		or32	$$⊢\left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\vee x=y\right)$$
15		orordir	$$⊢\left(\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\vee x=y\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
16	14 15	bitri	$$⊢\left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
17	13 16	bitri	$$⊢\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee x=y\right)\vee \left(y\underset{\dot{}}{<}x\vee x=y\right)\right)$$
18	12 17	bitr4di	$$⊢\left(K\in \mathrm{Poset}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
19	18	2ralbidva	$$⊢K\in \mathrm{Poset}\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{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
20	19	pm5.32i	$$⊢\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)\leftrightarrow \left(K\in \mathrm{Poset}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
21	1 2 3	pospo	$$⊢K\in V\to \left(K\in \mathrm{Poset}\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Po}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\right)$$
22	21	anbi1d	$$⊢K\in V\to \left(\left(K\in \mathrm{Poset}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)\right)$$
23	20 22	syl5bb	$$⊢K\in V\to \left(\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)\leftrightarrow \left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)\right)$$
24	1 2	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)$$
25		df-so	$$⊢\underset{\dot{}}{<}\mathrm{Or}B\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Po}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
26	25	anbi1i	$$⊢\left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\leftrightarrow \left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)$$
27		an32	$$⊢\left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\leftrightarrow \left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
28	26 27	bitri	$$⊢\left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\leftrightarrow \left(\left(\underset{\dot{}}{<}\mathrm{Po}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\right)$$
29	23 24 28	3bitr4g	$$⊢K\in V\to \left(K\in \mathrm{Toset}\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq \underset{\dot{}}{\le }\right)\right)$$