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

Metamath Proof Explorer

Theorem tsrlin

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

Ref Expression
Hypothesis istsr.1 ⊢ 𝑋 = dom 𝑅
Assertion tsrlin ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 istsr.1 ⊢ 𝑋 = dom 𝑅
2 1 istsr2 ⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
3 2 simprbi ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
4 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝑦 ) )
5 breq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐴 ) )
6 4 5 orbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝐴 𝑅 𝑦 ∨ 𝑦 𝑅 𝐴 ) ) )
7 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
8 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝐴 ↔ 𝐵 𝑅 𝐴 ) )
9 7 8 orbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝑅 𝑦 ∨ 𝑦 𝑅 𝐴 ) ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) ) )
10 6 9 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) ) )
11 3 10 syl5com ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) ) )
12 11 3impib ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) )