Theorem func2nd

Description: Extract the second 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	func2nd	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)=G$$

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		op2ndg	$$⊢\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\to 2^{nd}\left(⟨F,G⟩\right)=G$$
5	1 3 4	3syl	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)=G$$