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 HrmOp 0 hop op T x 0 T x ih x

Proof

Step Hyp Ref Expression
1 0hmop 0 hop HrmOp
2 leop 0 hop HrmOp T HrmOp 0 hop op T x 0 T - op 0 hop x ih x
3 1 2 mpan T HrmOp 0 hop op T x 0 T - op 0 hop x ih x
4 hmopf T HrmOp T :
5 hosubid1 T : T - op 0 hop = T
6 4 5 syl T HrmOp T - op 0 hop = T
7 6 fveq1d T HrmOp T - op 0 hop x = T x
8 7 oveq1d T HrmOp T - op 0 hop x ih x = T x ih x
9 8 breq2d T HrmOp 0 T - op 0 hop x ih x 0 T x ih x
10 9 ralbidv T HrmOp x 0 T - op 0 hop x ih x x 0 T x ih x
11 3 10 bitrd T HrmOp 0 hop op T x 0 T x ih x