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 
|- ( ph -> F ( C Func D ) G )
Assertion func2nd 
|- ( ph -> ( 2nd ` <. F , G >. ) = G )

Proof

Step Hyp Ref Expression
1 func1st.1 
 |-  ( ph -> F ( C Func D ) G )
2 relfunc 
 |-  Rel ( C Func D )
3 2 brrelex12i 
 |-  ( F ( C Func D ) G -> ( F e. _V /\ G e. _V ) )
4 op2ndg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 2nd ` <. F , G >. ) = G )
5 1 3 4 3syl 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )