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 ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐺 ‘ 𝐷 ) = ( 𝐶 𝐹 𝐷 ) )