Metamath Proof Explorer

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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
		natideq.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
		natideq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
		natcoeq.o	⊢ ⚬ = ( comp ‘ 𝐷 )
		natcoeq.x	⊢ · = ( comp ‘ 𝑄 )
		natcoeq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
		natcoeq.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐺 𝑁 𝐻 ) )
		natcoeq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 𝑁 𝐻 ) )
	Assertion	natcoeq	⊢ ( 𝜑 → ( 𝐿 = ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ⚬ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		natideq.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		natideq.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		natideq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		natcoeq.o	⊢ ⚬ = ( comp ‘ 𝐷 )
5		natcoeq.x	⊢ · = ( comp ‘ 𝑄 )
6		natcoeq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
7		natcoeq.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐺 𝑁 𝐻 ) )
8		natcoeq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 𝑁 𝐻 ) )
9	1 2 5 6 7	fuccocl	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ∈ ( 𝐹 𝑁 𝐻 ) )
10	2 3 8 9	nateq	⊢ ( 𝜑 → ( 𝐿 = ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ‘ 𝑥 ) ) )
11	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ ( 𝐺 𝑁 𝐻 ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
14	1 2 3 4 5 11 12 13	fuccoval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ⚬ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑥 ) ) )
15	14	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ⚬ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
16	15	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ⚬ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
17	10 16	bitrd	⊢ ( 𝜑 → ( 𝐿 = ( 𝑅 ( ⟨ 𝐹 , 𝐺 ⟩ · 𝐻 ) 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐿 ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ⚬ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )