up1st2nd

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

		Ref	Expression
	Hypothesis	up1st2nd.1	No typesetting found for \|- ( ph -> X ( F ( D UP E ) W ) M ) with typecode \|-
	Assertion	up1st2nd	Could not format assertion : No typesetting found for \|- ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M ) with typecode \|-

Step	Hyp	Ref	Expression
1		up1st2nd.1	Could not format ( ph -> X ( F ( D UP E ) W ) M ) : No typesetting found for \|- ( ph -> X ( F ( D UP E ) W ) M ) with typecode \|-
2		relfunc	$⊢ Rel (D Func E)$
3		df-br	Could not format ( X ( F ( D UP E ) W ) M <-> <. X , M >. e. ( F ( D UP E ) W ) ) : No typesetting found for \|- ( X ( F ( D UP E ) W ) M <-> <. X , M >. e. ( F ( D UP E ) W ) ) with typecode \|-
4	1 3	sylib	Could not format ( ph -> <. X , M >. e. ( F ( D UP E ) W ) ) : No typesetting found for \|- ( ph -> <. X , M >. e. ( F ( D UP E ) W ) ) with typecode \|-
5		eqid	$⊢ {Base}_{E} = {Base}_{E}$
6	5	uprcl	Could not format ( <. X , M >. e. ( F ( D UP E ) W ) -> ( F e. ( D Func E ) /\ W e. ( Base ` E ) ) ) : No typesetting found for \|- ( <. X , M >. e. ( F ( D UP E ) W ) -> ( F e. ( D Func E ) /\ W e. ( Base ` E ) ) ) with typecode \|-
7	4 6	syl	$⊢ φ \to (F \in (D Func E) \land W \in {Base}_{E})$
8	7	simpld	$⊢ φ \to F \in (D Func E)$
9		1st2nd	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
10	2 8 9	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
11	10	oveq1d	Could not format ( ph -> ( F ( D UP E ) W ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) ) : No typesetting found for \|- ( ph -> ( F ( D UP E ) W ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) ) with typecode \|-
12	11 1	breqdi	Could not format ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M ) : No typesetting found for \|- ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M ) with typecode \|-

Metamath Proof Explorer