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

Metamath Proof Explorer

Theorem curry2val

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

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

Proof

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