Theorem natcoeq

Description: A natural transformation equals a composite exactly when all its components equal the corresponding composites, including when the object set is empty. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	natideq.q	|- Q = ( C FuncCat D )
	natideq.n	|- N = ( C Nat D )
	natideq.b	|- B = ( Base ` C )
	natcoeq.o	|- .o. = ( comp ` D )
	natcoeq.x	|- .x. = ( comp ` Q )
	natcoeq.a	|- ( ph -> A e. ( F N G ) )
	natcoeq.r	|- ( ph -> R e. ( G N H ) )
	natcoeq.l	|- ( ph -> L e. ( F N H ) )
Assertion	natcoeq	|- ( ph -> ( L = ( R ( <. F , G >. .x. H ) A ) <-> A. x e. B ( L ` x ) = ( ( R ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .o. ( ( 1st ` H ) ` x ) ) ( A ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		natideq.q	|- Q = ( C FuncCat D )
2		natideq.n	|- N = ( C Nat D )
3		natideq.b	|- B = ( Base ` C )
4		natcoeq.o	|- .o. = ( comp ` D )
5		natcoeq.x	|- .x. = ( comp ` Q )
6		natcoeq.a	|- ( ph -> A e. ( F N G ) )
7		natcoeq.r	|- ( ph -> R e. ( G N H ) )
8		natcoeq.l	|- ( ph -> L e. ( F N H ) )
9	1 2 5 6 7	fuccocl	|- ( ph -> ( R ( <. F , G >. .x. H ) A ) e. ( F N H ) )
10	2 3 8 9	nateq	|- ( ph -> ( L = ( R ( <. F , G >. .x. H ) A ) <-> A. x e. B ( L ` x ) = ( ( R ( <. F , G >. .x. H ) A ) ` x ) ) )
11	6	adantr	|- ( ( ph /\ x e. B ) -> A e. ( F N G ) )
12	7	adantr	|- ( ( ph /\ x e. B ) -> R e. ( G N H ) )
13		simpr	|- ( ( ph /\ x e. B ) -> x e. B )
14	1 2 3 4 5 11 12 13	fuccoval	|- ( ( ph /\ x e. B ) -> ( ( R ( <. F , G >. .x. H ) A ) ` x ) = ( ( R ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .o. ( ( 1st ` H ) ` x ) ) ( A ` x ) ) )
15	14	eqeq2d	|- ( ( ph /\ x e. B ) -> ( ( L ` x ) = ( ( R ( <. F , G >. .x. H ) A ) ` x ) <-> ( L ` x ) = ( ( R ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .o. ( ( 1st ` H ) ` x ) ) ( A ` x ) ) ) )
16	15	ralbidva	|- ( ph -> ( A. x e. B ( L ` x ) = ( ( R ( <. F , G >. .x. H ) A ) ` x ) <-> A. x e. B ( L ` x ) = ( ( R ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .o. ( ( 1st ` H ) ` x ) ) ( A ` x ) ) ) )
17	10 16	bitrd	|- ( ph -> ( L = ( R ( <. F , G >. .x. H ) A ) <-> A. x e. B ( L ` x ) = ( ( R ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .o. ( ( 1st ` H ) ` x ) ) ( A ` x ) ) ) )