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

Metamath Proof Explorer

Theorem curry2f

Description: Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008)

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

Proof

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