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

Metamath Proof Explorer

Theorem tleile

Description: In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 tleile.b ⊢ B = Base K
2 tleile.l ⊢ ≤ ˙ = ≤ K
3 simp2 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X ∈ B
4 simp3 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
5 1 2 istos ⊢ K ∈ Toset ↔ K ∈ Poset ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ∨ y ≤ ˙ x
6 5 simprbi ⊢ K ∈ Toset → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ∨ y ≤ ˙ x
7 6 3ad2ant1 ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ∨ y ≤ ˙ x
8 breq1 ⊢ x = X → x ≤ ˙ y ↔ X ≤ ˙ y
9 breq2 ⊢ x = X → y ≤ ˙ x ↔ y ≤ ˙ X
10 8 9 orbi12d ⊢ x = X → x ≤ ˙ y ∨ y ≤ ˙ x ↔ X ≤ ˙ y ∨ y ≤ ˙ X
11 breq2 ⊢ y = Y → X ≤ ˙ y ↔ X ≤ ˙ Y
12 breq1 ⊢ y = Y → y ≤ ˙ X ↔ Y ≤ ˙ X
13 11 12 orbi12d ⊢ y = Y → X ≤ ˙ y ∨ y ≤ ˙ X ↔ X ≤ ˙ Y ∨ Y ≤ ˙ X
14 10 13 rspc2va ⊢ X ∈ B ∧ Y ∈ B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ∨ y ≤ ˙ x → X ≤ ˙ Y ∨ Y ≤ ˙ X
15 3 4 7 14 syl21anc ⊢ K ∈ Toset ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∨ Y ≤ ˙ X