Metamath Proof Explorer

Definition df-so

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 ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 1 0 wor wff R Or A
3 1 0 wpo wff R Po A
4 vx setvar x
5 vy setvar y
6 4 cv setvar x
7 5 cv setvar y
8 6 7 0 wbr wff x R y
9 6 7 wceq wff x = y
10 7 6 0 wbr wff y R x
11 8 9 10 w3o wff x R y ∨ x = y ∨ y R x
12 11 5 1 wral wff ∀ y ∈ A x R y ∨ x = y ∨ y R x
13 12 4 1 wral wff ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
14 3 13 wa wff R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
15 2 14 wb wff R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x