Theorem func1st

Description: Extract the first member of a functor. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypothesis	func1st.1	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	func1st	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$

Proof

Step	Hyp	Ref	Expression
1		func1st.1	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
2		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
3	2	brrelex12i	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
4		op1stg	$$⊢\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\to 1^{st}\left(⟨F,G⟩\right)=F$$
5	1 3 4	3syl	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$