Theorem upcic

Description: A universal property defines an object up to isomorphism given its existence. (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 ) )
	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	upcic	|- ( ph -> X ( ~=c ` D ) Y )

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	simpld	|- ( ph -> X ( ~=c ` D ) Y )