Metamath Proof Explorer

Theorem up1st2nd

Description: Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Hypothesis up1st2nd.1 
|- ( ph -> X ( F ( D UP E ) W ) M )
Assertion up1st2nd 
|- ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M )

Proof

Step Hyp Ref Expression
1 up1st2nd.1 
 |-  ( ph -> X ( F ( D UP E ) W ) M )
2 relfunc 
 |-  Rel ( D Func E )
3 df-br 
 |-  ( X ( F ( D UP E ) W ) M <-> <. X , M >. e. ( F ( D UP E ) W ) )
4 1 3 sylib 
 |-  ( ph -> <. X , M >. e. ( F ( D UP E ) W ) )
5 eqid 
 |-  ( Base ` E ) = ( Base ` E )
6 5 uprcl 
 |-  ( <. X , M >. e. ( F ( D UP E ) W ) -> ( F e. ( D Func E ) /\ W e. ( Base ` E ) ) )
7 4 6 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ W e. ( Base ` E ) ) )
8 7 simpld 
 |-  ( ph -> F e. ( D Func E ) )
9 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
10 2 8 9 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
11 10 oveq1d 
 |-  ( ph -> ( F ( D UP E ) W ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) )
12 11 1 breqdi 
 |-  ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M )