Metamath Proof Explorer

Theorem up1st2nd2

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

Ref Expression
Hypothesis up1st2nd2.1 
|- ( ph -> X e. ( F ( D UP E ) W ) )
Assertion up1st2nd2 
|- ( ph -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) )

Proof

Step Hyp Ref Expression
1 up1st2nd2.1 
 |-  ( ph -> X e. ( F ( D UP E ) W ) )
2 relup 
 |-  Rel ( F ( D UP E ) W )
3 1st2ndbr 
 |-  ( ( Rel ( F ( D UP E ) W ) /\ X e. ( F ( D UP E ) W ) ) -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) )
4 2 1 3 sylancr 
 |-  ( ph -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) )