This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{K}$
		tleile.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		tltnle.s	$⊢ \underset{˙}{<} = <_{K}$
	Assertion	tltnle	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow \neg Y \underset{˙}{\leq} X)$

Proof

Step	Hyp	Ref	Expression
1		tleile.b	$⊢ B = {Base}_{K}$
2		tleile.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		tltnle.s	$⊢ \underset{˙}{<} = <_{K}$
4		tospos	$⊢ K \in Toset \to K \in Poset$
5	1 2 3	pltval3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X))$
6	4 5	syl3an1	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X))$
7	1 2	tleile	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X)$
8		ibar	$⊢ (X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X) \to (\neg Y \underset{˙}{\leq} X \leftrightarrow ((X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X) \land \neg Y \underset{˙}{\leq} X))$
9		pm5.61	$⊢ ((X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X) \land \neg Y \underset{˙}{\leq} X) \leftrightarrow (X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X)$
10	8 9	bitr2di	$⊢ (X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X) \to ((X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X) \leftrightarrow \neg Y \underset{˙}{\leq} X)$
11	7 10	syl	$⊢ (K \in Toset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X) \leftrightarrow \neg Y \underset{˙}{\leq} X)$
12	6 11	bitrd	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow \neg Y \underset{˙}{\leq} X)$