Metamath Proof Explorer

Theorem adjeu

Description: Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion adjeu 
|- ( T : ~H --> ~H -> ( T e. dom adjh <-> E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 fex2 
 |-  ( ( T : ~H --> ~H /\ ~H e. _V /\ ~H e. _V ) -> T e. _V )
3 1 1 2 mp3an23 
 |-  ( T : ~H --> ~H -> T e. _V )
4 feq1 
 |-  ( t = T -> ( t : ~H --> ~H <-> T : ~H --> ~H ) )
5 fveq1 
 |-  ( t = T -> ( t ` y ) = ( T ` y ) )
6 5 oveq2d 
 |-  ( t = T -> ( x .ih ( t ` y ) ) = ( x .ih ( T ` y ) ) )
7 6 eqeq1d 
 |-  ( t = T -> ( ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
8 7 2ralbidv 
 |-  ( t = T -> ( A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
9 4 8 3anbi13d 
 |-  ( t = T -> ( ( 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 ) ) ) )
10 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 ) ) ) )
11 9 10 bitrdi 
 |-  ( t = T -> ( ( 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 ) ) ) ) )
12 11 exbidv 
 |-  ( t = 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 ) ) <-> E. u ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) )
13 19.42v 
 |-  ( E. u ( 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 /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
14 12 13 bitrdi 
 |-  ( t = 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 ) ) <-> ( T : ~H --> ~H /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) )
15 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 ) ) }
16 15 dmeqi 
 |-  dom adjh = dom { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
17 dmopab 
 |-  dom { <. 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 | E. u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
18 16 17 eqtri 
 |-  dom adjh = { 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 ) ) }
19 14 18 elab2g 
 |-  ( T e. _V -> ( T e. dom adjh <-> ( T : ~H --> ~H /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) )
20 19 baibd 
 |-  ( ( T e. _V /\ T : ~H --> ~H ) -> ( T e. dom adjh <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
21 3 20 mpancom 
 |-  ( T : ~H --> ~H -> ( T e. dom adjh <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
22 df-reu 
 |-  ( E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> E! u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
23 1 1 elmap 
 |-  ( u e. ( ~H ^m ~H ) <-> u : ~H --> ~H )
24 23 anbi1i 
 |-  ( ( u e. ( ~H ^m ~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 ) ) )
25 24 eubii 
 |-  ( E! u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
26 adjmo 
 |-  E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) )
27 df-eu 
 |-  ( E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
28 26 27 mpbiran2 
 |-  ( E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
29 22 25 28 3bitri 
 |-  ( E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
30 21 29 bitr4di 
 |-  ( T : ~H --> ~H -> ( T e. dom adjh <-> E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )