Metamath Proof Explorer

Theorem upeu2

Description: Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-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 ) )
upeu2.i 
|- I = ( Iso ` D )
upeu2.k 
|- ( ph -> K e. ( X I Y ) )
upeu2.n 
|- ( ph -> N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
Assertion upeu2 
|- ( ph -> ( N e. ( Z J ( F ` Y ) ) /\ A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) )

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 upeu2.i 
 |-  I = ( Iso ` D )
13 upeu2.k 
 |-  ( ph -> K e. ( X I Y ) )
14 upeu2.n 
 |-  ( ph -> N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
15 6 funcrcl3 
 |-  ( ph -> E e. Cat )
16 1 2 6 funcf1 
 |-  ( ph -> F : B --> C )
17 16 7 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. C )
18 16 8 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. C )
19 1 3 4 6 7 8 funcf2 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
20 6 funcrcl2 
 |-  ( ph -> D e. Cat )
21 1 3 12 20 7 8 isohom 
 |-  ( ph -> ( X I Y ) C_ ( X H Y ) )
22 21 13 sseldd 
 |-  ( ph -> K e. ( X H Y ) )
23 19 22 ffvelcdmd 
 |-  ( ph -> ( ( X G Y ) ` K ) e. ( ( F ` X ) J ( F ` Y ) ) )
24 2 4 5 15 9 17 18 10 23 catcocl 
 |-  ( ph -> ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) e. ( Z J ( F ` Y ) ) )
25 14 24 eqeltrd 
 |-  ( ph -> N e. ( Z J ( F ` Y ) ) )
26 11 adantr 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> 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 ) )
27 simprl 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> v e. B )
28 simprr 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> g e. ( Z J ( F ` v ) ) )
29 26 27 28 upciclem1 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> E! p e. ( X H v ) g = ( ( ( X G v ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) )
30 eqid 
 |-  ( comp ` D ) = ( comp ` D )
31 20 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> D e. Cat )
32 7 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> X e. B )
33 8 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> Y e. B )
34 27 adantr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> v e. B )
35 22 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> K e. ( X H Y ) )
36 simpr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> l e. ( Y H v ) )
37 1 3 30 31 32 33 34 35 36 catcocl 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ l e. ( Y H v ) ) -> ( l ( <. X , Y >. ( comp ` D ) v ) K ) e. ( X H v ) )
38 20 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> D e. Cat )
39 7 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> X e. B )
40 8 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> Y e. B )
41 27 adantr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> v e. B )
42 13 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> K e. ( X I Y ) )
43 simpr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> p e. ( X H v ) )
44 1 3 30 12 38 39 40 41 42 43 upeu2lem 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ p e. ( X H v ) ) -> E! l e. ( Y H v ) p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) )
45 simprr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) )
46 45 fveq2d 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> ( ( X G v ) ` p ) = ( ( X G v ) ` ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) )
47 46 oveq1d 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> ( ( ( X G v ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) = ( ( ( X G v ) ` ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) )
48 6 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> F ( D Func E ) G )
49 7 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> X e. B )
50 8 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> Y e. B )
51 27 adantr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> v e. B )
52 9 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> Z e. C )
53 10 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> M e. ( Z J ( F ` X ) ) )
54 22 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> K e. ( X H Y ) )
55 simprl 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> l e. ( Y H v ) )
56 14 ad2antrr 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
57 1 2 3 4 5 48 49 50 51 52 53 30 54 55 56 upciclem2 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> ( ( ( X G v ) ` ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
58 47 57 eqtrd 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> ( ( ( X G v ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
59 58 eqeq2d 
 |-  ( ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) /\ ( l e. ( Y H v ) /\ p = ( l ( <. X , Y >. ( comp ` D ) v ) K ) ) ) -> ( g = ( ( ( X G v ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) <-> g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) )
60 37 44 59 reuxfr1dd 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> ( E! p e. ( X H v ) g = ( ( ( X G v ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` v ) ) M ) <-> E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) )
61 29 60 mpbid 
 |-  ( ( ph /\ ( v e. B /\ g e. ( Z J ( F ` v ) ) ) ) -> E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
62 61 ralrimivva 
 |-  ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
63 25 62 jca 
 |-  ( ph -> ( N e. ( Z J ( F ` Y ) ) /\ A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) )