Theorem tleile

Description: In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Hypotheses	tleile.b	$$⊢B={\mathrm{Base}}_K$$
	tleile.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	tleile	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)$$

Proof

Step	Hyp	Ref	Expression
1		tleile.b	$$⊢B={\mathrm{Base}}_K$$
2		tleile.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		simp2	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
4		simp3	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
5	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)$$
6	5	simprbi	$$⊢K\in \mathrm{Toset}\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
7	6	3ad2ant1	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
8		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
9		breq2	$$⊢x=X\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }X\right)$$
10	8 9	orbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(X\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }X\right)\right)$$
11		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
12		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }X\leftrightarrow Y\underset{\dot{}}{\le }X\right)$$
13	11 12	orbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }X\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)\right)$$
14	10 13	rspc2va	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)\to \left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)$$
15	3 4 7 14	syl21anc	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)$$