Metamath Proof Explorer

Theorem leoprf2

Description: The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoprf2 
|- ( T : ~H --> ~H -> T <_op T )

Proof

Step Hyp Ref Expression
1 hodid 
 |-  ( T : ~H --> ~H -> ( T -op T ) = 0hop )
2 0hmop 
 |-  0hop e. HrmOp
3 1 2 eqeltrdi 
 |-  ( T : ~H --> ~H -> ( T -op T ) e. HrmOp )
4 0le0 
 |-  0 <_ 0
5 1 adantr 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T -op T ) = 0hop )
6 5 fveq1d 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( T -op T ) ` x ) = ( 0hop ` x ) )
7 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
8 7 adantl 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( 0hop ` x ) = 0h )
9 6 8 eqtrd 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( T -op T ) ` x ) = 0h )
10 9 oveq1d 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( ( T -op T ) ` x ) .ih x ) = ( 0h .ih x ) )
11 hi01 
 |-  ( x e. ~H -> ( 0h .ih x ) = 0 )
12 11 adantl 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( 0h .ih x ) = 0 )
13 10 12 eqtr2d 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> 0 = ( ( ( T -op T ) ` x ) .ih x ) )
14 4 13 breqtrid 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> 0 <_ ( ( ( T -op T ) ` x ) .ih x ) )
15 14 ralrimiva 
 |-  ( T : ~H --> ~H -> A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) )
16 ax-hilex 
 |-  ~H e. _V
17 fex 
 |-  ( ( T : ~H --> ~H /\ ~H e. _V ) -> T e. _V )
18 16 17 mpan2 
 |-  ( T : ~H --> ~H -> T e. _V )
19 leopg 
 |-  ( ( T e. _V /\ T e. _V ) -> ( T <_op T <-> ( ( T -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) ) ) )
20 18 18 19 syl2anc 
 |-  ( T : ~H --> ~H -> ( T <_op T <-> ( ( T -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) ) ) )
21 3 15 20 mpbir2and 
 |-  ( T : ~H --> ~H -> T <_op T )