Metamath Proof Explorer

Theorem funadj

Description: Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion funadj 
|- Fun adjh

Proof

Step Hyp Ref Expression
1 funopab 
 |-  ( Fun { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } <-> A. t E* u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
2 adjmo 
 |-  E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) )
3 3simpc 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) -> ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
4 3 moimi 
 |-  ( E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) -> E* u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
5 2 4 ax-mp 
 |-  E* u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) )
6 1 5 mpgbir 
 |-  Fun { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
7 dfadj2 
 |-  adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
8 7 funeqi 
 |-  ( Fun adjh <-> Fun { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } )
9 6 8 mpbir 
 |-  Fun adjh