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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐵 𝑅 𝐴 ) )