Metamath Proof Explorer


Theorem curry2ima

Description: The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017)

Ref Expression
Hypothesis curry2ima.1
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
Assertion curry2ima
|- ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G " D ) = { y | E. x e. D y = ( x F C ) } )

Proof

Step Hyp Ref Expression
1 curry2ima.1
 |-  G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
2 simp1
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> F Fn ( A X. B ) )
3 dffn2
 |-  ( F Fn ( A X. B ) <-> F : ( A X. B ) --> _V )
4 2 3 sylib
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> F : ( A X. B ) --> _V )
5 simp2
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> C e. B )
6 1 curry2f
 |-  ( ( F : ( A X. B ) --> _V /\ C e. B ) -> G : A --> _V )
7 4 5 6 syl2anc
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> G : A --> _V )
8 7 ffund
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> Fun G )
9 simp3
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> D C_ A )
10 7 fdmd
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> dom G = A )
11 9 10 sseqtrrd
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> D C_ dom G )
12 dfimafn
 |-  ( ( Fun G /\ D C_ dom G ) -> ( G " D ) = { y | E. x e. D ( G ` x ) = y } )
13 8 11 12 syl2anc
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G " D ) = { y | E. x e. D ( G ` x ) = y } )
14 1 curry2val
 |-  ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` x ) = ( x F C ) )
15 14 3adant3
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G ` x ) = ( x F C ) )
16 15 eqeq1d
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( ( G ` x ) = y <-> ( x F C ) = y ) )
17 eqcom
 |-  ( ( x F C ) = y <-> y = ( x F C ) )
18 16 17 bitrdi
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( ( G ` x ) = y <-> y = ( x F C ) ) )
19 18 rexbidv
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( E. x e. D ( G ` x ) = y <-> E. x e. D y = ( x F C ) ) )
20 19 abbidv
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> { y | E. x e. D ( G ` x ) = y } = { y | E. x e. D y = ( x F C ) } )
21 13 20 eqtrd
 |-  ( ( F Fn ( A X. B ) /\ C e. B /\ D C_ A ) -> ( G " D ) = { y | E. x e. D y = ( x F C ) } )