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 ROrARPoAxAyAxRyx=yyRx

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR classR
1 cA classA
2 1 0 wor wffROrA
3 1 0 wpo wffRPoA
4 vx setvarx
5 vy setvary
6 4 cv setvarx
7 5 cv setvary
8 6 7 0 wbr wffxRy
9 6 7 wceq wffx=y
10 7 6 0 wbr wffyRx
11 8 9 10 w3o wffxRyx=yyRx
12 11 5 1 wral wffyAxRyx=yyRx
13 12 4 1 wral wffxAyAxRyx=yyRx
14 3 13 wa wffRPoAxAyAxRyx=yyRx
15 2 14 wb wffROrARPoAxAyAxRyx=yyRx