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 ⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
Assertion curry1val ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐺 ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )

Proof

Step Hyp Ref Expression
1 curry1.1 ⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
2 1 curry1 ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )
3 2 fveq1d ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐺 ‘ 𝐷 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) )
4 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) )
5 4 fvmptndm ⊢ ( ¬ 𝐷 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ∅ )
6 5 adantl ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ ¬ 𝐷 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ∅ )
7 fndm ⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) )
8 7 adantr ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) )
9 simpr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → 𝐷 ∈ 𝐵 )
10 9 con3i ⊢ ( ¬ 𝐷 ∈ 𝐵 → ¬ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) )
11 ndmovg ⊢ ( ( dom 𝐹 = ( 𝐴 × 𝐵 ) ∧ ¬ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐶 𝐹 𝐷 ) = ∅ )
12 8 10 11 syl2an ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ ¬ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐹 𝐷 ) = ∅ )
13 6 12 eqtr4d ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ ¬ 𝐷 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )
14 13 ex ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ¬ 𝐷 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) ) )
15 oveq2 ⊢ ( 𝑥 = 𝐷 → ( 𝐶 𝐹 𝑥 ) = ( 𝐶 𝐹 𝐷 ) )
16 ovex ⊢ ( 𝐶 𝐹 𝐷 ) ∈ V
17 15 4 16 fvmpt ⊢ ( 𝐷 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )
18 14 17 pm2.61d2 ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )
19 3 18 eqtrd ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐺 ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )