This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 fovcdm 
 |-  ( ( 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 )