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 ⊢ 𝐵 = ( 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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋 ) )