# Metamath Proof Explorer

## Theorem curry1val

Description: The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis curry1.1 ${⊢}{G}={F}\circ {\left({{2}^{nd}↾}_{\left(\left\{{C}\right\}×\mathrm{V}\right)}\right)}^{-1}$
Assertion curry1val ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to {G}\left({D}\right)={C}{F}{D}$

### Proof

Step Hyp Ref Expression
1 curry1.1 ${⊢}{G}={F}\circ {\left({{2}^{nd}↾}_{\left(\left\{{C}\right\}×\mathrm{V}\right)}\right)}^{-1}$
2 1 curry1 ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to {G}=\left({x}\in {B}⟼{C}{F}{x}\right)$
3 2 fveq1d ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to {G}\left({D}\right)=\left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)$
4 eqid ${⊢}\left({x}\in {B}⟼{C}{F}{x}\right)=\left({x}\in {B}⟼{C}{F}{x}\right)$
5 4 fvmptndm ${⊢}¬{D}\in {B}\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)=\varnothing$
6 5 adantl ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\wedge ¬{D}\in {B}\right)\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)=\varnothing$
7 fndm ${⊢}{F}Fn\left({A}×{B}\right)\to \mathrm{dom}{F}={A}×{B}$
8 7 adantr ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to \mathrm{dom}{F}={A}×{B}$
9 simpr ${⊢}\left({C}\in {A}\wedge {D}\in {B}\right)\to {D}\in {B}$
10 9 con3i ${⊢}¬{D}\in {B}\to ¬\left({C}\in {A}\wedge {D}\in {B}\right)$
11 ndmovg ${⊢}\left(\mathrm{dom}{F}={A}×{B}\wedge ¬\left({C}\in {A}\wedge {D}\in {B}\right)\right)\to {C}{F}{D}=\varnothing$
12 8 10 11 syl2an ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\wedge ¬{D}\in {B}\right)\to {C}{F}{D}=\varnothing$
13 6 12 eqtr4d ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\wedge ¬{D}\in {B}\right)\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)={C}{F}{D}$
14 13 ex ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to \left(¬{D}\in {B}\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)={C}{F}{D}\right)$
15 oveq2 ${⊢}{x}={D}\to {C}{F}{x}={C}{F}{D}$
16 ovex ${⊢}{C}{F}{D}\in \mathrm{V}$
17 15 4 16 fvmpt ${⊢}{D}\in {B}\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)={C}{F}{D}$
18 14 17 pm2.61d2 ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to \left({x}\in {B}⟼{C}{F}{x}\right)\left({D}\right)={C}{F}{D}$
19 3 18 eqtrd ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {A}\right)\to {G}\left({D}\right)={C}{F}{D}$