Metamath Proof Explorer

Theorem ajmoi

Description: Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ip2eqi.1 
|- X = ( BaseSet ` U )
ip2eqi.7 
|- P = ( .iOLD ` U )
ip2eqi.u 
|- U e. CPreHilOLD
Assertion ajmoi 
|- E* s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) )

Proof

Step Hyp Ref Expression
1 ip2eqi.1 
 |-  X = ( BaseSet ` U )
2 ip2eqi.7 
 |-  P = ( .iOLD ` U )
3 ip2eqi.u 
 |-  U e. CPreHilOLD
4 r19.26-2 
 |-  ( A. x e. X A. y e. Y ( ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) <-> ( A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) )
5 eqtr2 
 |-  ( ( ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) -> ( x P ( s ` y ) ) = ( x P ( t ` y ) ) )
6 5 2ralimi 
 |-  ( A. x e. X A. y e. Y ( ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) -> A. x e. X A. y e. Y ( x P ( s ` y ) ) = ( x P ( t ` y ) ) )
7 4 6 sylbir 
 |-  ( ( A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) -> A. x e. X A. y e. Y ( x P ( s ` y ) ) = ( x P ( t ` y ) ) )
8 1 2 3 phoeqi 
 |-  ( ( s : Y --> X /\ t : Y --> X ) -> ( A. x e. X A. y e. Y ( x P ( s ` y ) ) = ( x P ( t ` y ) ) <-> s = t ) )
9 8 biimpa 
 |-  ( ( ( s : Y --> X /\ t : Y --> X ) /\ A. x e. X A. y e. Y ( x P ( s ` y ) ) = ( x P ( t ` y ) ) ) -> s = t )
10 7 9 sylan2 
 |-  ( ( ( s : Y --> X /\ t : Y --> X ) /\ ( A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) ) -> s = t )
11 10 an4s 
 |-  ( ( ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) /\ ( t : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) ) -> s = t )
12 11 gen2 
 |-  A. s A. t ( ( ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) /\ ( t : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) ) -> s = t )
13 feq1 
 |-  ( s = t -> ( s : Y --> X <-> t : Y --> X ) )
14 fveq1 
 |-  ( s = t -> ( s ` y ) = ( t ` y ) )
15 14 oveq2d 
 |-  ( s = t -> ( x P ( s ` y ) ) = ( x P ( t ` y ) ) )
16 15 eqeq2d 
 |-  ( s = t -> ( ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) <-> ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) )
17 16 2ralbidv 
 |-  ( s = t -> ( A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) <-> A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) )
18 13 17 anbi12d 
 |-  ( s = t -> ( ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) <-> ( t : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) ) )
19 18 mo4 
 |-  ( E* s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) <-> A. s A. t ( ( ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) /\ ( t : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( t ` y ) ) ) ) -> s = t ) )
20 12 19 mpbir 
 |-  E* s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) )