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 1 st V × C -1
Assertion curry2ima F Fn A × B C B D A G D = y | x D y = x F C

Proof

Step Hyp Ref Expression
1 curry2ima.1 G = F 1 st V × C -1
2 simp1 F Fn A × B C B D A F Fn A × B
3 dffn2 F Fn A × B F : A × B V
4 2 3 sylib F Fn A × B C B D A F : A × B V
5 simp2 F Fn A × B C B D A C B
6 1 curry2f F : A × B V C B G : A V
7 4 5 6 syl2anc F Fn A × B C B D A G : A V
8 7 ffund F Fn A × B C B D A Fun G
9 simp3 F Fn A × B C B D A D A
10 7 fdmd F Fn A × B C B D A dom G = A
11 9 10 sseqtrrd F Fn A × B C B D A D dom G
12 dfimafn Fun G D dom G G D = y | x D G x = y
13 8 11 12 syl2anc F Fn A × B C B D A G D = y | x D G x = y
14 1 curry2val F Fn A × B C B G x = x F C
15 14 3adant3 F Fn A × B C B D A G x = x F C
16 15 eqeq1d F Fn A × B C B D 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 × B C B D A G x = y y = x F C
19 18 rexbidv F Fn A × B C B D A x D G x = y x D y = x F C
20 19 abbidv F Fn A × B C B D A y | x D G x = y = y | x D y = x F C
21 13 20 eqtrd F Fn A × B C B D A G D = y | x D y = x F C