Theorem tlt2

Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018)

	Ref	Expression
Hypotheses	tlt2.b	$$⊢B={\mathrm{Base}}_K$$
	tlt2.e	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	tlt2.l	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	tlt2	$$⊢\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{}}{<}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		tlt2.b	$$⊢B={\mathrm{Base}}_K$$
2		tlt2.e	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		tlt2.l	$$⊢\underset{\dot{}}{<}={<}_K$$
4		exmidd	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\vee \neg X\underset{\dot{}}{\le }Y\right)$$
5	1 2 3	tltnle	$$⊢\left(K\in \mathrm{Toset}\wedge Y\in B\wedge X\in B\right)\to \left(Y\underset{\dot{}}{<}X\leftrightarrow \neg X\underset{\dot{}}{\le }Y\right)$$
6	5	3com23	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{<}X\leftrightarrow \neg X\underset{\dot{}}{\le }Y\right)$$
7	6	orbi2d	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{<}X\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\vee \neg X\underset{\dot{}}{\le }Y\right)\right)$$
8	4 7	mpbird	$$⊢\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{}}{<}X\right)$$