Metamath Proof Explorer

Theorem tsrlin

Description: A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis istsr.1 ⊢ X = dom ⁡ R
Assertion tsrlin ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X → A R B ∨ B R A

Proof

Step Hyp Ref Expression
1 istsr.1 ⊢ X = dom ⁡ R
2 1 istsr2 ⊢ R ∈ TosetRel ↔ R ∈ PosetRel ∧ ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x
3 2 simprbi ⊢ R ∈ TosetRel → ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x
4 breq1 ⊢ x = A → x R y ↔ A R y
5 breq2 ⊢ x = A → y R x ↔ y R A
6 4 5 orbi12d ⊢ x = A → x R y ∨ y R x ↔ A R y ∨ y R A
7 breq2 ⊢ y = B → A R y ↔ A R B
8 breq1 ⊢ y = B → y R A ↔ B R A
9 7 8 orbi12d ⊢ y = B → A R y ∨ y R A ↔ A R B ∨ B R A
10 6 9 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x → A R B ∨ B R A
11 3 10 syl5com ⊢ R ∈ TosetRel → A ∈ X ∧ B ∈ X → A R B ∨ B R A
12 11 3impib ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X → A R B ∨ B R A