Theorem uprcl

Description: Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025)

	Ref	Expression
Hypothesis	uprcl.c	|- C = ( Base ` E )
Assertion	uprcl	|- ( X e. ( F ( D UP E ) W ) -> ( F e. ( D Func E ) /\ W e. C ) )

Proof

Step	Hyp	Ref	Expression
1		uprcl.c	|- C = ( Base ` E )
2		eqid	|- ( Base ` D ) = ( Base ` D )
3		eqid	|- ( Hom ` D ) = ( Hom ` D )
4		eqid	|- ( Hom ` E ) = ( Hom ` E )
5		eqid	|- ( comp ` E ) = ( comp ` E )
6	2 1 3 4 5	upfval	|- ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. 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	elmpocl	|- ( X e. ( F ( D UP E ) W ) -> ( F e. ( D Func E ) /\ W e. C ) )