Theorem offun

Description: The function operation produces a function. (Contributed by SN, 23-Jul-2024)

	Ref	Expression
Hypotheses	offun.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offun.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	offun.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offun.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	offun	⊢ ( 𝜑 → Fun ( 𝐹 ∘f 𝑅 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		offun.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		offun.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		offun.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		offun.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		eqid	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 )
6	1 2 3 4 5	offn	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) Fn ( 𝐴 ∩ 𝐵 ) )
7		fnfun	⊢ ( ( 𝐹 ∘f 𝑅 𝐺 ) Fn ( 𝐴 ∩ 𝐵 ) → Fun ( 𝐹 ∘f 𝑅 𝐺 ) )
8	6 7	syl	⊢ ( 𝜑 → Fun ( 𝐹 ∘f 𝑅 𝐺 ) )