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\mathrm{FuncCat}D$$
	natideq.n	$$⊢N=C\mathrm{Nat}D$$
	natideq.b	$$⊢B={\mathrm{Base}}_C$$
	natcoeq.o	No typesetting found for |- .o. = ( comp ` D ) with typecode |-
	natcoeq.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(Q\right)$$
	natcoeq.a	$$⊢\phi \to A\in \left(FNG\right)$$
	natcoeq.r	$$⊢\phi \to R\in \left(GNH\right)$$
	natcoeq.l	$$⊢\phi \to L\in \left(FNH\right)$$
Assertion	natcoeq	Could not format assertion : No typesetting found for |- ( 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 ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		natideq.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		natideq.n	$$⊢N=C\mathrm{Nat}D$$
3		natideq.b	$$⊢B={\mathrm{Base}}_C$$
4		natcoeq.o	Could not format .o. = ( comp ` D ) : No typesetting found for |- .o. = ( comp ` D ) with typecode |-
5		natcoeq.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(Q\right)$$
6		natcoeq.a	$$⊢\phi \to A\in \left(FNG\right)$$
7		natcoeq.r	$$⊢\phi \to R\in \left(GNH\right)$$
8		natcoeq.l	$$⊢\phi \to L\in \left(FNH\right)$$
9	1 2 5 6 7	fuccocl	$$⊢\phi \to R\left(⟨F,G⟩\underset{\dot{}}{·}H\right)A\in \left(FNH\right)$$
10	2 3 8 9	nateq	$$⊢\phi \to \left(L=R\left(⟨F,G⟩\underset{\dot{}}{·}H\right)A\leftrightarrow \forall x\in BL\left(x\right)=\left(R\left(⟨F,G⟩\underset{\dot{}}{·}H\right)A\right)\left(x\right)\right)$$
11	6	adantr	$$⊢\left(\phi \wedge x\in B\right)\to A\in \left(FNG\right)$$
12	7	adantr	$$⊢\left(\phi \wedge x\in B\right)\to R\in \left(GNH\right)$$
13		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
14	1 2 3 4 5 11 12 13	fuccoval	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
15	14	eqeq2d	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
16	15	ralbidva	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
17	10 16	bitrd	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-