Definition df-leop 28711

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.)

Assertion

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

Distinct variable group:   u, t, x

Detailed syntax breakdown of Definition df-leop

Step	Hyp	Ref	Expression
1		cleo 27815	. 2 class <_op
2		vu	. . . . . . 7 setvar u
3	2	cv 1482	. . . . . 6 class u
4		vt	. . . . . . 7 setvar t
5	4	cv 1482	. . . . . 6 class t
6		chod 27797	. . . . . 6 class -op
7	3, 5, 6	co 6650	. . . . 5 class ( u -op t )
8		cho 27807	. . . . 5 class HrmOp
9	7, 8	wcel 1990	. . . 4 wff ( u -op t ) e. HrmOp
10		cc0 9936	. . . . . 6 class 0
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1482	. . . . . . . 8 class x
13	12, 7	cfv 5888	. . . . . . 7 class ( ( u -op t ) ` x )
14		csp 27779	. . . . . . 7 class .ih
15	13, 12, 14	co 6650	. . . . . 6 class ( ( ( u -op t ) ` x ) .ih x )
16		cle 10075	. . . . . 6 class <_
17	10, 15, 16	wbr 4653	. . . . 5 wff 0 <_ ( ( ( u -op t ) ` x ) .ih x )
18		chil 27776	. . . . 5 class ~H
19	17, 11, 18	wral 2912	. . . 4 wff A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x )
20	9, 19	wa 384	. . 3 wff ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) )
21	20, 4, 2	copab 4712	. 2 class { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }
22	1, 21	wceq 1483	1 wff <_op = { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }

This definition is referenced by:  leopg  28981