Definition df-leop 10058

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.

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 9102	. 2 class <_op
2		vu	. . . . . . 7 set u
3	2	cv 991	. . . . . 6 class u
4		vt	. . . . . . 7 set t
5	4	cv 991	. . . . . 6 class t
6		chod 9084	. . . . . 6 class -op
7	3, 5, 6	co 4021	. . . . 5 class (u -op t)
8		cho 9094	. . . . 5 class HrmOp
9	7, 8	wcel 994	. . . 4 wff (u -op t) e. HrmOp
10		cc0 5388	. . . . . 6 class 0
11		vx	. . . . . . . . 9 set x
12	11	cv 991	. . . . . . . 8 class x
13	12, 7	cfv 3263	. . . . . . 7 class ((u -op t)` x)
14		csp 9068	. . . . . . 7 class .ih
15	13, 12, 14	co 4021	. . . . . 6 class (((u -op t)` x) .ih x)
16		cle 5449	. . . . . 6 class <_
17	10, 15, 16	wbr 2692	. . . . 5 wff 0 <_ (((u -op t)` x) .ih x)
18		chil 9063	. . . . 5 class H~
19	17, 11, 18	wral 1691	. . . 4 wff A.x e. H~ 0 <_ (((u -op t)` x) .ih x)
20	9, 19	wa 221	. . 3 wff ((u -op t) e. HrmOp /\ A.x e. H~ 0 <_ (((u -op t)` x) .ih x))
21	20, 4, 2	copab 2740	. 2 class {<.t, u>. | ((u -op t) e. HrmOp /\ A.x e. H~ 0 <_ (((u -op t)` x) .ih x))}
22	1, 21	wceq 992	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 10335

Copyright terms: Public domain