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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tleile.l	⊢ ≤ = ( le ‘ 𝐾 )
	tltnle.s	⊢ < = ( lt ‘ 𝐾 )
Assertion	tltnle	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		tleile.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tleile.l	⊢ ≤ = ( le ‘ 𝐾 )
3		tltnle.s	⊢ < = ( lt ‘ 𝐾 )
4		tospos	⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
5	1 2 3	pltval3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ) )
6	4 5	syl3an1	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ) )
7	1 2	tleile	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) )
8		ibar	⊢ ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ) )
9		pm5.61	⊢ ( ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) )
10	8 9	bitr2di	⊢ ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ↔ ¬ 𝑌 ≤ 𝑋 ) )
11	7 10	syl	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ↔ ¬ 𝑌 ≤ 𝑋 ) )
12	6 11	bitrd	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋 ) )