Theorem fuco23alem

Description: The naturality property ( nati ) in category E . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco23a.a	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
	fuco23a.b	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
	fuco23a.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	fuco23alem.o	⊢ · = ( comp ‘ 𝐸 )
Assertion	fuco23alem	⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ · ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ · ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco23a.a	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
2		fuco23a.b	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
3		fuco23a.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
4		fuco23alem.o	⊢ · = ( comp ‘ 𝐸 )
5		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
10	9 1	natrcl2	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
11	8 6 10	funcf1	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
12	11 3	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
13	9 1	natrcl3	⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
14	8 6 13	funcf1	⊢ ( 𝜑 → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
15	14 3	ffvelcdmd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
16	9 1 8 7 3	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑋 ) ) )
17	5 2 6 7 4 12 15 16	nati	⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ · ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ · ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )