Metamath Proof Explorer

Theorem uprcl4

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 )
uprcl4.b 
|- B = ( Base ` D )
Assertion uprcl4 
|- ( ph -> X e. B )

Proof

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