Metamath Proof Explorer

Theorem uprcl5

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

Ref Expression
Hypotheses uprcl2.x 
|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
uprcl5.j 
|- J = ( Hom ` E )
Assertion uprcl5 
|- ( ph -> M e. ( W J ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 uprcl2.x 
 |-  ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
2 uprcl5.j 
 |-  J = ( Hom ` E )
3 eqid 
 |-  ( Base ` D ) = ( Base ` D )
4 eqid 
 |-  ( Base ` E ) = ( Base ` E )
5 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
6 eqid 
 |-  ( comp ` E ) = ( comp ` E )
7 1 4 uprcl3 
 |-  ( ph -> W e. ( Base ` E ) )
8 1 uprcl2 
 |-  ( ph -> F ( D Func E ) G )
9 3 4 5 2 6 7 8 isuplem 
 |-  ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. ( Base ` D ) /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. ( Base ` D ) A. g e. ( W J ( F ` y ) ) E! k e. ( X ( Hom ` D ) y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` y ) ) M ) ) ) )
10 1 9 mpbid 
 |-  ( ph -> ( ( X e. ( Base ` D ) /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. ( Base ` D ) A. g e. ( W J ( F ` y ) ) E! k e. ( X ( Hom ` D ) y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` y ) ) M ) ) )
11 10 simplrd 
 |-  ( ph -> M e. ( W J ( F ` X ) ) )