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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	natideq.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natideq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	natideq.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	natideq.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
	natideq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐹 ) )
Assertion	natideq	⊢ ( 𝜑 → ( 𝐴 = ( 𝐼 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		natideq.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		natideq.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		natideq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		natideq.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
5		natideq.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
6		natideq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐹 ) )
7	2	natrcl	⊢ ( 𝐴 ∈ ( 𝐹 𝑁 𝐹 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) )
9	8	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
10	1 4 5 9	fucid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( 𝐽 ∘ ( 1^st ‘ 𝐹 ) ) )
11	1 2 5 9	fucidcl	⊢ ( 𝜑 → ( 𝐽 ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 𝑁 𝐹 ) )
12	10 11	eqeltrd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) ∈ ( 𝐹 𝑁 𝐹 ) )
13	2 3 6 12	nateq	⊢ ( 𝜑 → ( 𝐴 = ( 𝐼 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝐹 ) ‘ 𝑥 ) ) )
14	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ 𝐹 ) = ( 𝐽 ∘ ( 1^st ‘ 𝐹 ) ) )
15	14	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝐽 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) )
16		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
17	9	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
18	3 16 17	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
21	19 20	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐽 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
22	15 21	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
23	22	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝐹 ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
24	23	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝐹 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
25	13 24	bitrd	⊢ ( 𝜑 → ( 𝐴 = ( 𝐼 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐽 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem natideq

Proof