Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ajval Structured version   Unicode version

Theorem ajval 26479
 Description: Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
Hypotheses
Ref Expression
ajval.1
ajval.2
ajval.3
ajval.4
ajval.5
Assertion
Ref Expression
ajval
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,
Allowed substitution hints:   (,,)   (,,)   (,,)   ()

Proof of Theorem ajval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 phnv 26431 . . . . 5
2 ajval.1 . . . . . 6
3 ajval.2 . . . . . 6
4 ajval.3 . . . . . 6
5 ajval.4 . . . . . 6
6 ajval.5 . . . . . 6
72, 3, 4, 5, 6ajfval 26426 . . . . 5
81, 7sylan 473 . . . 4
98fveq1d 5875 . . 3
11 fvex 5883 . . . . . . 7
122, 11eqeltri 2504 . . . . . 6
13 fex 6145 . . . . . 6
1412, 13mpan2 675 . . . . 5
15 eqid 2420 . . . . . 6
16 feq1 5720 . . . . . . 7
17 fveq1 5872 . . . . . . . . . 10
1817oveq1d 6312 . . . . . . . . 9
1918eqeq1d 2422 . . . . . . . 8
20192ralbidv 2867 . . . . . . 7
2116, 203anbi13d 1337 . . . . . 6
2215, 21fvopab5 5981 . . . . 5
2314, 22syl 17 . . . 4
24 3anass 986 . . . . . 6
2524baib 911 . . . . 5
2625iotabidv 5578 . . . 4
2723, 26eqtrd 2461 . . 3