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

Metamath Proof Explorer

Theorem curry1f

Description: Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008)

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

Proof

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