Metamath Proof Explorer

Theorem isuplem

Description: Lemma for isup and other theorems. (Contributed by Zhi Wang, 25-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 )
Assertion 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 ) ) ) )

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 1 2 3 4 5 6 7 upfval3 
 |-  ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , 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 ) ) } )
9 oveq1 
 |-  ( x = X -> ( x H y ) = ( X H y ) )
10 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
11 10 opeq2d 
 |-  ( x = X -> <. W , ( F ` x ) >. = <. W , ( F ` X ) >. )
12 11 oveq1d 
 |-  ( x = X -> ( <. W , ( F ` x ) >. O ( F ` y ) ) = ( <. W , ( F ` X ) >. O ( F ` y ) ) )
13 oveq1 
 |-  ( x = X -> ( x G y ) = ( X G y ) )
14 13 fveq1d 
 |-  ( x = X -> ( ( x G y ) ` k ) = ( ( X G y ) ` k ) )
15 eqidd 
 |-  ( x = X -> m = m )
16 12 14 15 oveq123d 
 |-  ( x = X -> ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) )
17 16 eqeq2d 
 |-  ( x = X -> ( g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) <-> g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) ) )
18 9 17 reueqbidv 
 |-  ( x = X -> ( E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) <-> E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) ) )
19 18 2ralbidv 
 |-  ( x = 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 ) <-> 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 ) ) )
20 oveq2 
 |-  ( m = M -> ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) )
21 20 eqeq2d 
 |-  ( m = M -> ( g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) <-> g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) )
22 21 reubidv 
 |-  ( m = M -> ( E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) m ) <-> E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) )
23 22 2ralbidv 
 |-  ( m = 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 ) <-> 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 ) ) )
24 eqidd 
 |-  ( ( x = X /\ m = M ) -> B = B )
25 simpl 
 |-  ( ( x = X /\ m = M ) -> x = X )
26 25 fveq2d 
 |-  ( ( x = X /\ m = M ) -> ( F ` x ) = ( F ` X ) )
27 26 oveq2d 
 |-  ( ( x = X /\ m = M ) -> ( W J ( F ` x ) ) = ( W J ( F ` X ) ) )
28 8 19 23 24 27 brab2ddw 
 |-  ( 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 ) ) ) )