Metamath Proof Explorer

Theorem func1st

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

Ref Expression
Hypothesis func1st.1 
|- ( ph -> F ( C Func D ) G )
Assertion func1st 
|- ( ph -> ( 1st ` <. F , G >. ) = F )

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 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
5 1 3 4 3syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )