Theorem natideq

Description: A natural transformation is an identity exactly when all its components are identities. This also covers an empty object set. (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$$
	natideq.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
	natideq.j	$$⊢J=\mathrm{Id}\left(D\right)$$
	natideq.a	$$⊢\phi \to A\in \left(FNF\right)$$
Assertion	natideq	$$⊢\phi \to \left(A=I\left(F\right)\leftrightarrow \forall x\in BA\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$

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		natideq.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
5		natideq.j	$$⊢J=\mathrm{Id}\left(D\right)$$
6		natideq.a	$$⊢\phi \to A\in \left(FNF\right)$$
7	2	natrcl	$$⊢A\in \left(FNF\right)\to \left(F\in \left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)$$
8	6 7	syl	$$⊢\phi \to \left(F\in \left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)$$
9	8	simpld	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
10	1 4 5 9	fucid	$$⊢\phi \to I\left(F\right)=J\circ 1^{st}\left(F\right)$$
11	1 2 5 9	fucidcl	$$⊢\phi \to J\circ 1^{st}\left(F\right)\in \left(FNF\right)$$
12	10 11	eqeltrd	$$⊢\phi \to I\left(F\right)\in \left(FNF\right)$$
13	2 3 6 12	nateq	$$⊢\phi \to \left(A=I\left(F\right)\leftrightarrow \forall x\in BA\left(x\right)=I\left(F\right)\left(x\right)\right)$$
14	10	adantr	$$⊢\left(\phi \wedge x\in B\right)\to I\left(F\right)=J\circ 1^{st}\left(F\right)$$
15	14	fveq1d	$$⊢\left(\phi \wedge x\in B\right)\to I\left(F\right)\left(x\right)=\left(J\circ 1^{st}\left(F\right)\right)\left(x\right)$$
16		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
17	9	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
18	3 16 17	funcf1	$$⊢\phi \to 1^{st}\left(F\right):B⟶{\mathrm{Base}}_D$$
19	18	adantr	$$⊢\left(\phi \wedge x\in B\right)\to 1^{st}\left(F\right):B⟶{\mathrm{Base}}_D$$
20		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
21	19 20	fvco3d	$$⊢\left(\phi \wedge x\in B\right)\to \left(J\circ 1^{st}\left(F\right)\right)\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)$$
22	15 21	eqtrd	$$⊢\left(\phi \wedge x\in B\right)\to I\left(F\right)\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)$$
23	22	eqeq2d	$$⊢\left(\phi \wedge x\in B\right)\to \left(A\left(x\right)=I\left(F\right)\left(x\right)\leftrightarrow A\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
24	23	ralbidva	$$⊢\phi \to \left(\forall x\in BA\left(x\right)=I\left(F\right)\left(x\right)\leftrightarrow \forall x\in BA\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
25	13 24	bitrd	$$⊢\phi \to \left(A=I\left(F\right)\leftrightarrow \forall x\in BA\left(x\right)=J\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$