This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upeu

Description: A universal property defines an essentially unique (strong form) pair of object X and morphism M if it exists. (Contributed by Zhi Wang, 19-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 ) )
upcic.n 
|- ( ph -> N e. ( Z J ( F ` Y ) ) )
upcic.2 
|- ( 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 ) )
Assertion upeu 
|- ( ph -> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )

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 upcic.n 
 |-  ( ph -> N e. ( Z J ( F ` Y ) ) )
13 upcic.2 
 |-  ( 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 ) )
14 1 2 3 4 5 6 7 8 9 10 11 12 13 upciclem4 
 |-  ( ph -> ( X ( ~=c ` D ) Y /\ E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
15 14 simprd 
 |-  ( ph -> E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
16 eqid 
 |-  ( Iso ` D ) = ( Iso ` D )
17 6 funcrcl2 
 |-  ( ph -> D e. Cat )
18 1 3 16 17 7 8 isohom 
 |-  ( ph -> ( X ( Iso ` D ) Y ) C_ ( X H Y ) )
19 11 8 12 upciclem1 
 |-  ( ph -> E! r e. ( X H Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
20 reurmo 
 |-  ( E! r e. ( X H Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) -> E* r e. ( X H Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
21 19 20 syl 
 |-  ( ph -> E* r e. ( X H Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
22 nfcv 
 |-  F/_ r ( X ( Iso ` D ) Y )
23 nfcv 
 |-  F/_ r ( X H Y )
24 22 23 ssrmof 
 |-  ( ( X ( Iso ` D ) Y ) C_ ( X H Y ) -> ( E* r e. ( X H Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) -> E* r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
25 18 21 24 sylc 
 |-  ( ph -> E* r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
26 reu5 
 |-  ( E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) <-> ( E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) /\ E* r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
27 15 25 26 sylanbrc 
 |-  ( ph -> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )