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

Metamath Proof Explorer

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 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) )
13 equequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑧 = 𝑦 ) )
14 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 ) )
15 12 13 14 3orbi123d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑧 𝑅 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
16 15 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑧 𝑅 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
17 16 rspw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
18 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑧 ) )
19 equequ2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
20 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
21 18 19 20 3orbi123d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) )
22 21 rspw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
23 17 22 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) )
24 23 impd ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
25 11 24 simplbiim ⊢ ( 𝑅 Or 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
26 25 com12 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
27 5 10 26 vtocl2ga ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
28 27 impcom ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) )