Metamath Proof Explorer


Theorem curry2f

Description: Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis curry2.1
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
Assertion curry2f
|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D )

Proof

Step Hyp Ref Expression
1 curry2.1
 |-  G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
2 ffn
 |-  ( F : ( A X. B ) --> D -> F Fn ( A X. B ) )
3 1 curry2
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
4 2 3 sylan
 |-  ( ( F : ( A X. B ) --> D /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
5 fovrn
 |-  ( ( F : ( A X. B ) --> D /\ x e. A /\ C e. B ) -> ( x F C ) e. D )
6 5 3com23
 |-  ( ( F : ( A X. B ) --> D /\ C e. B /\ x e. A ) -> ( x F C ) e. D )
7 6 3expa
 |-  ( ( ( F : ( A X. B ) --> D /\ C e. B ) /\ x e. A ) -> ( x F C ) e. D )
8 4 7 fmpt3d
 |-  ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D )