Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-leop Structured version   Unicode version

Definition df-leop 23355
 Description: Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that means that is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-leop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-leop
StepHypRef Expression
1 cleo 22461 . 2
2 vu . . . . . . 7
32cv 1651 . . . . . 6
4 vt . . . . . . 7
54cv 1651 . . . . . 6
6 chod 22443 . . . . . 6
73, 5, 6co 6081 . . . . 5
8 cho 22453 . . . . 5
97, 8wcel 1725 . . . 4
10 cc0 8990 . . . . . 6
11 vx . . . . . . . . 9
1211cv 1651 . . . . . . . 8
1312, 7cfv 5454 . . . . . . 7
14 csp 22425 . . . . . . 7
1513, 12, 14co 6081 . . . . . 6
16 cle 9121 . . . . . 6
1710, 15, 16wbr 4212 . . . . 5
18 chil 22422 . . . . 5
1917, 11, 18wral 2705 . . . 4
209, 19wa 359 . . 3
2120, 4, 2copab 4265 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  leopg  23625
 Copyright terms: Public domain W3C validator