Theorem curry1f

Description: Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008)

	Ref	Expression
Hypothesis	curry1.1	⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
Assertion	curry1f	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 ∧ 𝐶 ∈ 𝐴 ) → 𝐺 : 𝐵 ⟶ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		curry1.1	⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
2		ffn	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
3	1	curry1	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )
4	2 3	sylan	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )
5		fovrn	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 ∧ 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 𝐹 𝑥 ) ∈ 𝐷 )
6	5	3expa	⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 𝐹 𝑥 ) ∈ 𝐷 )
7	4 6	fmpt3d	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 ∧ 𝐶 ∈ 𝐴 ) → 𝐺 : 𝐵 ⟶ 𝐷 )