Metamath Proof Explorer

Theorem leoppos

Description: Binary relation defining a positive operator. Definition VI.1 of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoppos 
|- ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )

Proof

Step Hyp Ref Expression
1 0hmop 
 |-  0hop e. HrmOp
2 leop 
 |-  ( ( 0hop e. HrmOp /\ T e. HrmOp ) -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( ( T -op 0hop ) ` x ) .ih x ) ) )
3 1 2 mpan 
 |-  ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( ( T -op 0hop ) ` x ) .ih x ) ) )
4 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
5 hosubid1 
 |-  ( T : ~H --> ~H -> ( T -op 0hop ) = T )
6 4 5 syl 
 |-  ( T e. HrmOp -> ( T -op 0hop ) = T )
7 6 fveq1d 
 |-  ( T e. HrmOp -> ( ( T -op 0hop ) ` x ) = ( T ` x ) )
8 7 oveq1d 
 |-  ( T e. HrmOp -> ( ( ( T -op 0hop ) ` x ) .ih x ) = ( ( T ` x ) .ih x ) )
9 8 breq2d 
 |-  ( T e. HrmOp -> ( 0 <_ ( ( ( T -op 0hop ) ` x ) .ih x ) <-> 0 <_ ( ( T ` x ) .ih x ) ) )
10 9 ralbidv 
 |-  ( T e. HrmOp -> ( A. x e. ~H 0 <_ ( ( ( T -op 0hop ) ` x ) .ih x ) <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )
11 3 10 bitrd 
 |-  ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )