Definition df-leop

Description: Define positive operator ordering. Definition VI.1 of Retherford p. 49. Note that ( ~H X. 0H ) <_op T means that T is a positive operator. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-leop	|- <_op = { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleo	|- <_op
1		vt	|- t
2		vu	|- u
3	2	cv	|- u
4		chod	|- -op
5	1	cv	|- t
6	3 5 4	co	|- ( u -op t )
7		cho	|- HrmOp
8	6 7	wcel	|- ( u -op t ) e. HrmOp
9		vx	|- x
10		chba	|- ~H
11		cc0	|- 0
12		cle	|- <_
13	9	cv	|- x
14	13 6	cfv	|- ( ( u -op t ) ` x )
15		csp	|- .ih
16	14 13 15	co	|- ( ( ( u -op t ) ` x ) .ih x )
17	11 16 12	wbr	|- 0 <_ ( ( ( u -op t ) ` x ) .ih x )
18	17 9 10	wral	|- A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x )
19	8 18	wa	|- ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) )
20	19 1 2	copab	|- { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }
21	0 20	wceq	|- <_op = { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }