Theorem upeu2lem

Description: Lemma for upeu2 . There exists a unique morphism from Y to Z that commutes if F : X --> Y is an isomorphism. (Contributed by Zhi Wang, 20-Sep-2025)

	Ref	Expression
Hypotheses	upeu2lem.b	|- B = ( Base ` C )
	upeu2lem.h	|- H = ( Hom ` C )
	upeu2lem.o	|- .x. = ( comp ` C )
	upeu2lem.i	|- I = ( Iso ` C )
	upeu2lem.c	|- ( ph -> C e. Cat )
	upeu2lem.x	|- ( ph -> X e. B )
	upeu2lem.y	|- ( ph -> Y e. B )
	upeu2lem.z	|- ( ph -> Z e. B )
	upeu2lem.f	|- ( ph -> F e. ( X I Y ) )
	upeu2lem.g	|- ( ph -> G e. ( X H Z ) )
Assertion	upeu2lem	|- ( ph -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )

Proof

Step	Hyp	Ref	Expression
1		upeu2lem.b	|- B = ( Base ` C )
2		upeu2lem.h	|- H = ( Hom ` C )
3		upeu2lem.o	|- .x. = ( comp ` C )
4		upeu2lem.i	|- I = ( Iso ` C )
5		upeu2lem.c	|- ( ph -> C e. Cat )
6		upeu2lem.x	|- ( ph -> X e. B )
7		upeu2lem.y	|- ( ph -> Y e. B )
8		upeu2lem.z	|- ( ph -> Z e. B )
9		upeu2lem.f	|- ( ph -> F e. ( X I Y ) )
10		upeu2lem.g	|- ( ph -> G e. ( X H Z ) )
11	1 2 4 5 7 6	isohom	|- ( ph -> ( Y I X ) C_ ( Y H X ) )
12		eqid	|- ( Inv ` C ) = ( Inv ` C )
13	1 12 5 6 7 4	invf	|- ( ph -> ( X ( Inv ` C ) Y ) : ( X I Y ) --> ( Y I X ) )
14	13 9	ffvelcdmd	|- ( ph -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y I X ) )
15	11 14	sseldd	|- ( ph -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y H X ) )
16	1 2 3 5 7 6 8 15 10	catcocl	|- ( ph -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) e. ( Y H Z ) )
17		oveq1	|- ( G = ( k ( <. X , Y >. .x. Z ) F ) -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
18	17	adantl	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
19	5	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> C e. Cat )
20	7	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> Y e. B )
21	6	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> X e. B )
22	15	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y H X ) )
23	1 2 4 5 6 7	isohom	|- ( ph -> ( X I Y ) C_ ( X H Y ) )
24	23 9	sseldd	|- ( ph -> F e. ( X H Y ) )
25	24	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> F e. ( X H Y ) )
26	8	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> Z e. B )
27		simpr	|- ( ( ph /\ k e. ( Y H Z ) ) -> k e. ( Y H Z ) )
28	1 2 3 19 20 21 20 22 25 26 27	catass	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( k ( <. Y , Y >. .x. Z ) ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
29	9	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> F e. ( X I Y ) )
30		eqid	|- ( Id ` C ) = ( Id ` C )
31	3	oveqi	|- ( <. Y , X >. .x. Y ) = ( <. Y , X >. ( comp ` C ) Y )
32	1 4 12 19 21 20 29 30 31	isocoinvid	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( Id ` C ) ` Y ) )
33	32	oveq2d	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( k ( <. Y , Y >. .x. Z ) ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) = ( k ( <. Y , Y >. .x. Z ) ( ( Id ` C ) ` Y ) ) )
34	1 2 30 19 20 3 26 27	catrid	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( k ( <. Y , Y >. .x. Z ) ( ( Id ` C ) ` Y ) ) = k )
35	28 33 34	3eqtrd	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = k )
36	35	adantr	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = k )
37	18 36	eqtr2d	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
38		oveq1	|- ( k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) -> ( k ( <. X , Y >. .x. Z ) F ) = ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) )
39	38	adantl	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> ( k ( <. X , Y >. .x. Z ) F ) = ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) )
40	10	adantr	|- ( ( ph /\ k e. ( Y H Z ) ) -> G e. ( X H Z ) )
41	1 2 3 19 21 20 21 25 22 26 40	catass	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , X >. .x. Z ) ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) ) )
42	3	oveqi	|- ( <. X , Y >. .x. X ) = ( <. X , Y >. ( comp ` C ) X )
43	1 4 12 19 21 20 29 30 42	invcoisoid	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) = ( ( Id ` C ) ` X ) )
44	43	oveq2d	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( G ( <. X , X >. .x. Z ) ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) ) = ( G ( <. X , X >. .x. Z ) ( ( Id ` C ) ` X ) ) )
45	1 2 30 19 21 3 26 40	catrid	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( G ( <. X , X >. .x. Z ) ( ( Id ` C ) ` X ) ) = G )
46	41 44 45	3eqtrd	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = G )
47	46	adantr	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = G )
48	39 47	eqtr2d	|- ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> G = ( k ( <. X , Y >. .x. Z ) F ) )
49	37 48	impbida	|- ( ( ph /\ k e. ( Y H Z ) ) -> ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
50	49	ralrimiva	|- ( ph -> A. k e. ( Y H Z ) ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
51		reu6i	|- ( ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) e. ( Y H Z ) /\ A. k e. ( Y H Z ) ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) ) -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )
52	16 50 51	syl2anc	|- ( ph -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )