Metamath Proof Explorer

Theorem ajfuni

Description: The adjoint function is a function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajfuni.5 
|- A = ( U adj W )
ajfuni.u 
|- U e. CPreHilOLD
ajfuni.w 
|- W e. NrmCVec
Assertion ajfuni 
|- Fun A

Proof

Step Hyp Ref Expression
1 ajfuni.5 
 |-  A = ( U adj W )
2 ajfuni.u 
 |-  U e. CPreHilOLD
3 ajfuni.w 
 |-  W e. NrmCVec
4 funopab 
 |-  ( Fun { <. t , s >. | ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) } <-> A. t E* s ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) )
5 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
6 eqid 
 |-  ( .iOLD ` U ) = ( .iOLD ` U )
7 5 6 2 ajmoi 
 |-  E* s ( s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) )
8 3simpc 
 |-  ( ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) -> ( s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) )
9 8 moimi 
 |-  ( E* s ( s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) -> E* s ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) )
10 7 9 ax-mp 
 |-  E* s ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) )
11 4 10 mpgbir 
 |-  Fun { <. t , s >. | ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) }
12 2 phnvi 
 |-  U e. NrmCVec
13 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
14 eqid 
 |-  ( .iOLD ` W ) = ( .iOLD ` W )
15 5 13 6 14 1 ajfval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> A = { <. t , s >. | ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) } )
16 12 3 15 mp2an 
 |-  A = { <. t , s >. | ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) }
17 16 funeqi 
 |-  ( Fun A <-> Fun { <. t , s >. | ( t : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ s : ( BaseSet ` W ) --> ( BaseSet ` U ) /\ A. x e. ( BaseSet ` U ) A. y e. ( BaseSet ` W ) ( ( t ` x ) ( .iOLD ` W ) y ) = ( x ( .iOLD ` U ) ( s ` y ) ) ) } )
18 11 17 mpbir 
 |-  Fun A