Theorem func2nd

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

	Ref	Expression
Hypothesis	func1st.1	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion	func2nd	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		func1st.1	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
2		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
3	2	brrelex12i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
4		op2ndg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
5	1 3 4	3syl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )