This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem func2nd

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

		Ref	Expression
	Hypothesis	func1st.1	$⊢ φ \to F (C Func D) G$
	Assertion	func2nd	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$

Step	Hyp	Ref	Expression
1		func1st.1	$⊢ φ \to F (C Func D) G$
2		relfunc	$⊢ Rel (C Func D)$
3	2	brrelex12i	$⊢ F (C Func D) G \to (F \in V \land G \in V)$
4		op2ndg	$⊢ (F \in V \land G \in V) \to 2^{nd} (⟨F, G⟩) = G$
5	1 3 4	3syl	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$