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 = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleo	⊢ ≤op
1		vt	⊢ 𝑡
2		vu	⊢ 𝑢
3	2	cv	⊢ 𝑢
4		chod	⊢ −op
5	1	cv	⊢ 𝑡
6	3 5 4	co	⊢ ( 𝑢 −op 𝑡 )
7		cho	⊢ HrmOp
8	6 7	wcel	⊢ ( 𝑢 −op 𝑡 ) ∈ HrmOp
9		vx	⊢ 𝑥
10		chba	⊢ ℋ
11		cc0	⊢ 0
12		cle	⊢ ≤
13	9	cv	⊢ 𝑥
14	13 6	cfv	⊢ ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 )
15		csp	⊢ ·ih
16	14 13 15	co	⊢ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 )
17	11 16 12	wbr	⊢ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 )
18	17 9 10	wral	⊢ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 )
19	8 18	wa	⊢ ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) )
20	19 1 2	copab	⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ) }
21	0 20	wceq	⊢ ≤op = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ) }