Theorem func1st2nd

Description: Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypothesis	func1st2nd.1	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		func1st2nd.1	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
2		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
3		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
4	2 1 3	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$