Metamath Proof Explorer

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 ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cleo class ≤ op
1 vt setvar t
2 vu setvar u
3 2 cv setvar u
4 chod class - op
5 1 cv setvar t
6 3 5 4 co class u - op t
7 cho class HrmOp
8 6 7 wcel wff u - op t ∈ HrmOp
9 vx setvar x
10 chba class ℋ
11 cc0 class 0
12 cle class ≤
13 9 cv setvar x
14 13 6 cfv class u - op t ⁡ x
15 csp class ⋅ ih
16 14 13 15 co class u - op t ⁡ x ⋅ ih x
17 11 16 12 wbr wff 0 ≤ u - op t ⁡ x ⋅ ih x
18 17 9 10 wral wff ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x
19 8 18 wa wff u - op t ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x
20 19 1 2 copab class t u | u - op t ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x
21 0 20 wceq wff ≤ op = t u | u - op t ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x