Theorem tltnle

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

	Ref	Expression
Hypotheses	tleile.b	|- B = ( Base ` K )
	tleile.l	|- .<_ = ( le ` K )
	tltnle.s	|- .< = ( lt ` K )
Assertion	tltnle	|- ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> -. Y .<_ X ) )

Proof

Step	Hyp	Ref	Expression
1		tleile.b	|- B = ( Base ` K )
2		tleile.l	|- .<_ = ( le ` K )
3		tltnle.s	|- .< = ( lt ` K )
4		tospos	|- ( K e. Toset -> K e. Poset )
5	1 2 3	pltval3	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ -. Y .<_ X ) ) )
6	4 5	syl3an1	|- ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ -. Y .<_ X ) ) )
7	1 2	tleile	|- ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X .<_ Y \/ Y .<_ X ) )
8		ibar	|- ( ( X .<_ Y \/ Y .<_ X ) -> ( -. Y .<_ X <-> ( ( X .<_ Y \/ Y .<_ X ) /\ -. Y .<_ X ) ) )
9		pm5.61	|- ( ( ( X .<_ Y \/ Y .<_ X ) /\ -. Y .<_ X ) <-> ( X .<_ Y /\ -. Y .<_ X ) )
10	8 9	bitr2di	|- ( ( X .<_ Y \/ Y .<_ X ) -> ( ( X .<_ Y /\ -. Y .<_ X ) <-> -. Y .<_ X ) )
11	7 10	syl	|- ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ -. Y .<_ X ) <-> -. Y .<_ X ) )
12	6 11	bitrd	|- ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> -. Y .<_ X ) )