This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )