Metamath Proof Explorer

Theorem func1st2nd

Description: Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypothesis func1st2nd.1 
|- ( ph -> F e. ( C Func D ) )
Assertion func1st2nd 
|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )

Proof

Step Hyp Ref Expression
1 func1st2nd.1 
 |-  ( ph -> F e. ( C Func D ) )
2 relfunc 
 |-  Rel ( C Func D )
3 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
4 2 1 3 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )