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

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 ∘ 2 nd ↾ C × V -1
Assertion curry1val ⊢ F Fn A × B ∧ C ∈ A → G ⁡ D = C F D

Proof

Step Hyp Ref Expression
1 curry1.1 ⊢ G = F ∘ 2 nd ↾ C × V -1
2 1 curry1 ⊢ F Fn A × B ∧ C ∈ A → G = x ∈ B ⟼ C F x
3 2 fveq1d ⊢ F Fn A × B ∧ C ∈ A → G ⁡ D = x ∈ B ⟼ C F x ⁡ D
4 eqid ⊢ x ∈ B ⟼ C F x = x ∈ B ⟼ C F x
5 4 fvmptndm ⊢ ¬ D ∈ B → x ∈ B ⟼ C F x ⁡ D = ∅
6 5 adantl ⊢ F Fn A × B ∧ C ∈ A ∧ ¬ D ∈ B → x ∈ B ⟼ C F x ⁡ D = ∅
7 fndm ⊢ F Fn A × B → dom ⁡ F = A × B
8 7 adantr ⊢ F Fn A × B ∧ C ∈ A → dom ⁡ F = A × B
9 simpr ⊢ C ∈ A ∧ D ∈ B → D ∈ B
10 9 con3i ⊢ ¬ D ∈ B → ¬ C ∈ A ∧ D ∈ B
11 ndmovg ⊢ dom ⁡ F = A × B ∧ ¬ C ∈ A ∧ D ∈ B → C F D = ∅
12 8 10 11 syl2an ⊢ F Fn A × B ∧ C ∈ A ∧ ¬ D ∈ B → C F D = ∅
13 6 12 eqtr4d ⊢ F Fn A × B ∧ C ∈ A ∧ ¬ D ∈ B → x ∈ B ⟼ C F x ⁡ D = C F D
14 13 ex ⊢ F Fn A × B ∧ C ∈ A → ¬ D ∈ B → x ∈ B ⟼ C F x ⁡ D = C F D
15 oveq2 ⊢ x = D → C F x = C F D
16 ovex ⊢ C F D ∈ V
17 15 4 16 fvmpt ⊢ D ∈ B → x ∈ B ⟼ C F x ⁡ D = C F D
18 14 17 pm2.61d2 ⊢ F Fn A × B ∧ C ∈ A → x ∈ B ⟼ C F x ⁡ D = C F D
19 3 18 eqtrd ⊢ F Fn A × B ∧ C ∈ A → G ⁡ D = C F D