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 /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	wor	|- R Or A
3	1 0	wpo	|- R Po A
4		vx	|- x
5		vy	|- y
6	4	cv	|- x
7	5	cv	|- y
8	6 7 0	wbr	|- x R y
9	6 7	wceq	|- x = y
10	7 6 0	wbr	|- y R x
11	8 9 10	w3o	|- ( x R y \/ x = y \/ y R x )
12	11 5 1	wral	|- A. y e. A ( x R y \/ x = y \/ y R x )
13	12 4 1	wral	|- A. x e. A A. y e. A ( x R y \/ x = y \/ y R x )
14	3 13	wa	|- ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )
15	2 14	wb	|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )