Theorem ofcfn

Description: The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofcfval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcfval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	ofcfn	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		ofcfval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ofcfval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4		ovex	⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ∈ V
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) )
6	4 5	fnmpti	⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) Fn 𝐴
7		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8	1 2 3 7	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
9	8	fneq1d	⊢ ( 𝜑 → ( ( 𝐹 ∘f/c 𝑅 𝐶 ) Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) Fn 𝐴 ) )
10	6 9	mpbiri	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) Fn 𝐴 )