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

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 ) } )