Definition df-leop 9773

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 8822	. 2 class <_op
2		vu	. . . . . . 7 set u
3	2	cv 957	. . . . . 6 class u
4		vt	. . . . . . 7 set t
5	4	cv 957	. . . . . 6 class t
6		chod 8804	. . . . . 6 class -op
7	3, 5, 6	co 3969	. . . . 5 class (u -op t)
8		cho 8814	. . . . 5 class HrmOp
9	7, 8	wcel 960	. . . 4 wff (u -op t) e. HrmOp
10		cc0 5246	. . . . . 6 class 0
11		vx	. . . . . . . . 9 set x
12	11	cv 957	. . . . . . . 8 class x
13	12, 7	cfv 3188	. . . . . . 7 class ((u -op t)` x)
14		csp 8788	. . . . . . 7 class .ih
15	13, 12, 14	co 3969	. . . . . 6 class (((u -op t)` x) .ih x)
16		cle 5307	. . . . . 6 class <_
17	10, 15, 16	wbr 2624	. . . . 5 wff 0 <_ (((u -op t)` x) .ih x)
18		chil 8783	. . . . 5 class H~
19	17, 11, 18	wral 1648	. . . 4 wff A.x e. H~ 0 <_ (((u -op t)` x) .ih x)
20	9, 19	wa 223	. . 3 wff ((u -op t) e. HrmOp /\ A.x e. H~ 0 <_ (((u -op t)` x) .ih x))
21	20, 4, 2	copab 2671	. 2 class {<.t, u>. | ((u -op t) e. HrmOp /\ A.x e. H~ 0 <_ (((u -op t)` x) .ih x))}
22	1, 21	wceq 958	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 10050

Copyright terms: Public domain