Theorem isup

Description: The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	upfval.b	|- B = ( Base ` D )
	upfval.c	|- C = ( Base ` E )
	upfval.h	|- H = ( Hom ` D )
	upfval.j	|- J = ( Hom ` E )
	upfval.o	|- O = ( comp ` E )
	upfval2.w	|- ( ph -> W e. C )
	upfval3.f	|- ( ph -> F ( D Func E ) G )
	isup.x	|- ( ph -> X e. B )
	isup.m	|- ( ph -> M e. ( W J ( F ` X ) ) )
Assertion	isup	|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) )

Proof

Step	Hyp	Ref	Expression
1		upfval.b	|- B = ( Base ` D )
2		upfval.c	|- C = ( Base ` E )
3		upfval.h	|- H = ( Hom ` D )
4		upfval.j	|- J = ( Hom ` E )
5		upfval.o	|- O = ( comp ` E )
6		upfval2.w	|- ( ph -> W e. C )
7		upfval3.f	|- ( ph -> F ( D Func E ) G )
8		isup.x	|- ( ph -> X e. B )
9		isup.m	|- ( ph -> M e. ( W J ( F ` X ) ) )
10	8 9	jca	|- ( ph -> ( X e. B /\ M e. ( W J ( F ` X ) ) ) )
11	1 2 3 4 5 6 7	isuplem	|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) )
12	10 11	mpbirand	|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) )