Theorem isup2

Description: The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	isup2.b	|- B = ( Base ` D )
	isup2.h	|- H = ( Hom ` D )
	isup2.j	|- J = ( Hom ` E )
	isup2.o	|- O = ( comp ` E )
	isup2.x	|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
Assertion	isup2	|- ( ph -> 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		isup2.b	|- B = ( Base ` D )
2		isup2.h	|- H = ( Hom ` D )
3		isup2.j	|- J = ( Hom ` E )
4		isup2.o	|- O = ( comp ` E )
5		isup2.x	|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
6		eqid	|- ( Base ` E ) = ( Base ` E )
7	5 6	uprcl3	|- ( ph -> W e. ( Base ` E ) )
8	5	uprcl2	|- ( ph -> F ( D Func E ) G )
9	5 1	uprcl4	|- ( ph -> X e. B )
10	5 3	uprcl5	|- ( ph -> M e. ( W J ( F ` X ) ) )
11	1 6 2 3 4 7 8 9 10	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 ) ) )
12	5 11	mpbid	|- ( ph -> 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 ) )