Metamath Proof Explorer

Theorem uptrlem2

Description: Lemma for uptr . (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses uptrlem1.h 
|- H = ( Hom ` C )
uptrlem1.i 
|- I = ( Hom ` D )
uptrlem1.j 
|- J = ( Hom ` E )
uptrlem1.d 
|- .xb = ( comp ` D )
uptrlem1.e 
|- .o. = ( comp ` E )
uptrlem2.a 
|- A = ( Base ` C )
uptrlem2.b 
|- B = ( Base ` D )
uptrlem2.x 
|- ( ph -> X e. B )
uptrlem2.y 
|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
uptrlem2.z 
|- ( ph -> Z e. A )
uptrlem2.w 
|- ( ph -> W e. A )
uptrlem2.m 
|- ( ph -> M e. ( X I ( ( 1st ` F ) ` Z ) ) )
uptrlem2.n 
|- ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
uptrlem2.f 
|- ( ph -> F e. ( C Func D ) )
uptrlem2.k 
|- ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
uptrlem2.g 
|- ( ph -> ( K o.func F ) = G )
Assertion uptrlem2 
|- ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) )

Proof

Step Hyp Ref Expression
1 uptrlem1.h 
 |-  H = ( Hom ` C )
2 uptrlem1.i 
 |-  I = ( Hom ` D )
3 uptrlem1.j 
 |-  J = ( Hom ` E )
4 uptrlem1.d 
 |-  .xb = ( comp ` D )
5 uptrlem1.e 
 |-  .o. = ( comp ` E )
6 uptrlem2.a 
 |-  A = ( Base ` C )
7 uptrlem2.b 
 |-  B = ( Base ` D )
8 uptrlem2.x 
 |-  ( ph -> X e. B )
9 uptrlem2.y 
 |-  ( ph -> ( ( 1st ` K ) ` X ) = Y )
10 uptrlem2.z 
 |-  ( ph -> Z e. A )
11 uptrlem2.w 
 |-  ( ph -> W e. A )
12 uptrlem2.m 
 |-  ( ph -> M e. ( X I ( ( 1st ` F ) ` Z ) ) )
13 uptrlem2.n 
 |-  ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
14 uptrlem2.f 
 |-  ( ph -> F e. ( C Func D ) )
15 uptrlem2.k 
 |-  ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
16 uptrlem2.g 
 |-  ( ph -> ( K o.func F ) = G )
17 8 7 eleqtrdi 
 |-  ( ph -> X e. ( Base ` D ) )
18 10 6 eleqtrdi 
 |-  ( ph -> Z e. ( Base ` C ) )
19 11 6 eleqtrdi 
 |-  ( ph -> W e. ( Base ` C ) )
20 14 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
21 relfull 
 |-  Rel ( D Full E )
22 relin1 
 |-  ( Rel ( D Full E ) -> Rel ( ( D Full E ) i^i ( D Faith E ) ) )
23 21 22 ax-mp 
 |-  Rel ( ( D Full E ) i^i ( D Faith E ) )
24 1st2nd 
 |-  ( ( Rel ( ( D Full E ) i^i ( D Faith E ) ) /\ K e. ( ( D Full E ) i^i ( D Faith E ) ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
25 23 15 24 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
26 25 15 eqeltrrd 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( ( D Full E ) i^i ( D Faith E ) ) )
27 df-br 
 |-  ( ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) <-> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( ( D Full E ) i^i ( D Faith E ) ) )
28 26 27 sylibr 
 |-  ( ph -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) )
29 inss1 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Full E )
30 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
31 29 30 sstri 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Func E )
32 31 15 sselid 
 |-  ( ph -> K e. ( D Func E ) )
33 14 32 cofu1st2nd 
 |-  ( ph -> ( K o.func F ) = ( <. ( 1st ` K ) , ( 2nd ` K ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
34 relfunc 
 |-  Rel ( C Func E )
35 14 32 cofucl 
 |-  ( ph -> ( K o.func F ) e. ( C Func E ) )
36 16 35 eqeltrrd 
 |-  ( ph -> G e. ( C Func E ) )
37 1st2nd 
 |-  ( ( Rel ( C Func E ) /\ G e. ( C Func E ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
38 34 36 37 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
39 16 33 38 3eqtr3d 
 |-  ( ph -> ( <. ( 1st ` K ) , ( 2nd ` K ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) = <. ( 1st ` G ) , ( 2nd ` G ) >. )
40 1 2 3 4 5 17 9 18 19 12 13 20 28 39 uptrlem1 
 |-  ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) )