Metamath Proof Explorer

Theorem upciclem3

Description: Lemma for upciclem4 . (Contributed by Zhi Wang, 17-Sep-2025)

Ref Expression
Hypotheses upcic.b 
|- B = ( Base ` D )
upcic.c 
|- C = ( Base ` E )
upcic.h 
|- H = ( Hom ` D )
upcic.j 
|- J = ( Hom ` E )
upcic.o 
|- O = ( comp ` E )
upcic.f 
|- ( ph -> F ( D Func E ) G )
upcic.x 
|- ( ph -> X e. B )
upcic.y 
|- ( ph -> Y e. B )
upcic.z 
|- ( ph -> Z e. C )
upcic.m 
|- ( ph -> M e. ( Z J ( F ` X ) ) )
upcic.1 
|- ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) )
upciclem3.od 
|- .x. = ( comp ` D )
upciclem3.k 
|- ( ph -> K e. ( X H Y ) )
upciclem3.l 
|- ( ph -> L e. ( Y H X ) )
upciclem3.mn 
|- ( ph -> M = ( ( ( Y G X ) ` L ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
upciclem3.nm 
|- ( ph -> N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
Assertion upciclem3 
|- ( ph -> ( L ( <. X , Y >. .x. X ) K ) = ( ( Id ` D ) ` X ) )

Proof

Step Hyp Ref Expression
1 upcic.b 
 |-  B = ( Base ` D )
2 upcic.c 
 |-  C = ( Base ` E )
3 upcic.h 
 |-  H = ( Hom ` D )
4 upcic.j 
 |-  J = ( Hom ` E )
5 upcic.o 
 |-  O = ( comp ` E )
6 upcic.f 
 |-  ( ph -> F ( D Func E ) G )
7 upcic.x 
 |-  ( ph -> X e. B )
8 upcic.y 
 |-  ( ph -> Y e. B )
9 upcic.z 
 |-  ( ph -> Z e. C )
10 upcic.m 
 |-  ( ph -> M e. ( Z J ( F ` X ) ) )
11 upcic.1 
 |-  ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) )
12 upciclem3.od 
 |-  .x. = ( comp ` D )
13 upciclem3.k 
 |-  ( ph -> K e. ( X H Y ) )
14 upciclem3.l 
 |-  ( ph -> L e. ( Y H X ) )
15 upciclem3.mn 
 |-  ( ph -> M = ( ( ( Y G X ) ` L ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
16 upciclem3.nm 
 |-  ( ph -> N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
17 fveq2 
 |-  ( p = ( L ( <. X , Y >. .x. X ) K ) -> ( ( X G X ) ` p ) = ( ( X G X ) ` ( L ( <. X , Y >. .x. X ) K ) ) )
18 17 oveq1d 
 |-  ( p = ( L ( <. X , Y >. .x. X ) K ) -> ( ( ( X G X ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) = ( ( ( X G X ) ` ( L ( <. X , Y >. .x. X ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
19 18 eqeq2d 
 |-  ( p = ( L ( <. X , Y >. .x. X ) K ) -> ( M = ( ( ( X G X ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) <-> M = ( ( ( X G X ) ` ( L ( <. X , Y >. .x. X ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) ) )
20 fveq2 
 |-  ( p = ( ( Id ` D ) ` X ) -> ( ( X G X ) ` p ) = ( ( X G X ) ` ( ( Id ` D ) ` X ) ) )
21 20 oveq1d 
 |-  ( p = ( ( Id ` D ) ` X ) -> ( ( ( X G X ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) = ( ( ( X G X ) ` ( ( Id ` D ) ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
22 21 eqeq2d 
 |-  ( p = ( ( Id ` D ) ` X ) -> ( M = ( ( ( X G X ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) <-> M = ( ( ( X G X ) ` ( ( Id ` D ) ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) ) )
23 11 7 10 upciclem1 
 |-  ( ph -> E! p e. ( X H X ) M = ( ( ( X G X ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
24 6 funcrcl2 
 |-  ( ph -> D e. Cat )
25 1 3 12 24 7 8 7 13 14 catcocl 
 |-  ( ph -> ( L ( <. X , Y >. .x. X ) K ) e. ( X H X ) )
26 eqid 
 |-  ( Id ` D ) = ( Id ` D )
27 1 3 26 24 7 catidcl 
 |-  ( ph -> ( ( Id ` D ) ` X ) e. ( X H X ) )
28 1 2 3 4 5 6 7 8 7 9 10 12 13 14 16 upciclem2 
 |-  ( ph -> ( ( ( X G X ) ` ( L ( <. X , Y >. .x. X ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) = ( ( ( Y G X ) ` L ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
29 15 28 eqtr4d 
 |-  ( ph -> M = ( ( ( X G X ) ` ( L ( <. X , Y >. .x. X ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
30 eqid 
 |-  ( Id ` E ) = ( Id ` E )
31 1 26 30 6 7 funcid 
 |-  ( ph -> ( ( X G X ) ` ( ( Id ` D ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( X G X ) ` ( ( Id ` D ) ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) = ( ( ( Id ` E ) ` ( F ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
33 6 funcrcl3 
 |-  ( ph -> E e. Cat )
34 1 2 6 funcf1 
 |-  ( ph -> F : B --> C )
35 34 7 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. C )
36 2 4 30 33 9 5 35 10 catlid 
 |-  ( ph -> ( ( ( Id ` E ) ` ( F ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) = M )
37 32 36 eqtr2d 
 |-  ( ph -> M = ( ( ( X G X ) ` ( ( Id ` D ) ` X ) ) ( <. Z , ( F ` X ) >. O ( F ` X ) ) M ) )
38 19 22 23 25 27 29 37 reu2eqd 
 |-  ( ph -> ( L ( <. X , Y >. .x. X ) K ) = ( ( Id ` D ) ` X ) )