Theorem solin

Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996)

	Ref	Expression
Assertion	solin	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝐵 𝑅 𝑦 ) )
2		eqeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝑦 ↔ 𝐵 = 𝑦 ) )
3		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐵 ) )
4	1 2 3	3orbi123d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) )
5	4	imbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑅 Or 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) ) )
6		breq2	⊢ ( 𝑦 = 𝐶 → ( 𝐵 𝑅 𝑦 ↔ 𝐵 𝑅 𝐶 ) )
7		eqeq2	⊢ ( 𝑦 = 𝐶 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐶 ) )
8		breq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 𝑅 𝐵 ↔ 𝐶 𝑅 𝐵 ) )
9	6 7 8	3orbi123d	⊢ ( 𝑦 = 𝐶 → ( ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
10	9	imbi2d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) ↔ ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) ) )
11		df-so	⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
12		rsp2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
13	11 12	simplbiim	⊢ ( 𝑅 Or 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
14	13	com12	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
15	5 10 14	vtocl2ga	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
16	15	impcom	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) )