Theorem tltnle

Description: In a Toset, "less than" is equivalent to the negation of the converse of "less than or equal to", see pltnle . (Contributed by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Hypotheses	tleile.b	$$⊢B={\mathrm{Base}}_K$$
	tleile.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	tltnle.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	tltnle	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \neg 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		tltnle.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4		tospos	$$⊢K\in \mathrm{Toset}\to K\in \mathrm{Poset}$$
5	1 2 3	pltval3	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge \neg Y\underset{\dot{}}{\le }X\right)\right)$$
6	4 5	syl3an1	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge \neg Y\underset{\dot{}}{\le }X\right)\right)$$
7	1 2	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)$$
8		ibar	$$⊢\left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)\to \left(\neg Y\underset{\dot{}}{\le }X\leftrightarrow \left(\left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)\wedge \neg Y\underset{\dot{}}{\le }X\right)\right)$$
9		pm5.61	$$⊢\left(\left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)\wedge \neg Y\underset{\dot{}}{\le }X\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge \neg Y\underset{\dot{}}{\le }X\right)$$
10	8 9	bitr2di	$$⊢\left(X\underset{\dot{}}{\le }Y\vee Y\underset{\dot{}}{\le }X\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge \neg Y\underset{\dot{}}{\le }X\right)\leftrightarrow \neg Y\underset{\dot{}}{\le }X\right)$$
11	7 10	syl	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge \neg Y\underset{\dot{}}{\le }X\right)\leftrightarrow \neg Y\underset{\dot{}}{\le }X\right)$$
12	6 11	bitrd	$$⊢\left(K\in \mathrm{Toset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \neg Y\underset{\dot{}}{\le }X\right)$$