Description: Define the strict complete (linear) order predicate. The expression R Or A is true if relationship R orders A . For example, < Or RR is true ( ltso ). Equivalent to Definition 6.19(1) of TakeutiZaring p. 29. (Contributed by NM, 21-Jan-1996)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-so | ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | ⊢ 𝑅 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | 1 0 | wor | ⊢ 𝑅 Or 𝐴 |
| 3 | 1 0 | wpo | ⊢ 𝑅 Po 𝐴 |
| 4 | vx | ⊢ 𝑥 | |
| 5 | vy | ⊢ 𝑦 | |
| 6 | 4 | cv | ⊢ 𝑥 |
| 7 | 5 | cv | ⊢ 𝑦 |
| 8 | 6 7 0 | wbr | ⊢ 𝑥 𝑅 𝑦 |
| 9 | 6 7 | wceq | ⊢ 𝑥 = 𝑦 |
| 10 | 7 6 0 | wbr | ⊢ 𝑦 𝑅 𝑥 |
| 11 | 8 9 10 | w3o | ⊢ ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) |
| 12 | 11 5 1 | wral | ⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) |
| 13 | 12 4 1 | wral | ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) |
| 14 | 3 13 | wa | ⊢ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) |
| 15 | 2 14 | wb | ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |