Theorem relup

Description: The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025)

	Ref	Expression
Assertion	relup	|- Rel ( F ( D UP E ) W )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` D ) = ( Base ` D )
2		eqid	|- ( Base ` E ) = ( Base ` E )
3		eqid	|- ( Hom ` D ) = ( Hom ` D )
4		eqid	|- ( Hom ` E ) = ( Hom ` E )
5		eqid	|- ( comp ` E ) = ( comp ` E )
6	1 2 3 4 5	upfval	|- ( D UP E ) = ( f e. ( D Func E ) , w e. ( Base ` E ) |-> { <. x , m >. | ( ( x e. ( Base ` D ) /\ m e. ( w ( Hom ` E ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` D ) A. g e. ( w ( Hom ` E ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` D ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` E ) ( ( 1st ` f ) ` y ) ) m ) ) } )
7	6	relmpoopab	|- Rel ( F ( D UP E ) W )