Theorem offun

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

	Ref	Expression
Hypotheses	offun.1	$$⊢\phi \to FFnA$$
	offun.2	$$⊢\phi \to GFnB$$
	offun.3	$$⊢\phi \to A\in V$$
	offun.4	$$⊢\phi \to B\in W$$
Assertion	offun	$$⊢\phi \to \mathrm{Fun}\left(F{R}_{f}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		offun.1	$$⊢\phi \to FFnA$$
2		offun.2	$$⊢\phi \to GFnB$$
3		offun.3	$$⊢\phi \to A\in V$$
4		offun.4	$$⊢\phi \to B\in W$$
5		eqid	$$⊢A\cap B=A\cap B$$
6	1 2 3 4 5	offn	$$⊢\phi \to \left(F{R}_{f}G\right)Fn\left(A\cap B\right)$$
7		fnfun	$$⊢\left(F{R}_{f}G\right)Fn\left(A\cap B\right)\to \mathrm{Fun}\left(F{R}_{f}G\right)$$
8	6 7	syl	$$⊢\phi \to \mathrm{Fun}\left(F{R}_{f}G\right)$$