Metamath Proof Explorer

Theorem tlt3

Description: In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses tlt3.b ⊢ B = Base K
tlt3.l ⊢ < ˙ = < K
Assertion tlt3 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X = Y ∨ X < ˙ Y ∨ Y < ˙ X

Proof

Step Hyp Ref Expression
1 tlt3.b ⊢ B = Base K
2 tlt3.l ⊢ < ˙ = < K
3 eqid ⊢ ≤ K = ≤ K
4 1 3 2 tlt2 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∨ Y < ˙ X
5 tospos ⊢ K ∈ Toset → K ∈ Poset
6 1 3 2 pleval2 ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ↔ X < ˙ Y ∨ X = Y
7 orcom ⊢ X < ˙ Y ∨ X = Y ↔ X = Y ∨ X < ˙ Y
8 6 7 bitrdi ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ↔ X = Y ∨ X < ˙ Y
9 5 8 syl3an1 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ↔ X = Y ∨ X < ˙ Y
10 9 orbi1d ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∨ Y < ˙ X ↔ X = Y ∨ X < ˙ Y ∨ Y < ˙ X
11 4 10 mpbid ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X = Y ∨ X < ˙ Y ∨ Y < ˙ X
12 df-3or ⊢ X = Y ∨ X < ˙ Y ∨ Y < ˙ X ↔ X = Y ∨ X < ˙ Y ∨ Y < ˙ X
13 11 12 sylibr ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X = Y ∨ X < ˙ Y ∨ Y < ˙ X