Metamath Proof Explorer

Theorem dmadjss

Description: The domain of the adjoint function is a subset of the maps from ~H to ~H . (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjss 
|- dom adjh C_ ( ~H ^m ~H )

Proof

Step Hyp Ref Expression
1 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 ) ) }
2 3anass 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( t : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
3 ax-hilex 
 |-  ~H e. _V
4 3 3 elmap 
 |-  ( t e. ( ~H ^m ~H ) <-> t : ~H --> ~H )
5 4 anbi1i 
 |-  ( ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) <-> ( t : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
6 2 5 bitr4i 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
7 6 opabbii 
 |-  { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } = { <. t , u >. | ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) }
8 1 7 eqtri 
 |-  adjh = { <. t , u >. | ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) }
9 8 dmeqi 
 |-  dom adjh = dom { <. t , u >. | ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) }
10 dmopabss 
 |-  dom { <. t , u >. | ( t e. ( ~H ^m ~H ) /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) ) } C_ ( ~H ^m ~H )
11 9 10 eqsstri 
 |-  dom adjh C_ ( ~H ^m ~H )