Theorem fuchom

Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 14-Oct-2024)

	Ref	Expression
Hypotheses	fucbas.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuchom.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
Assertion	fuchom	⊢ 𝑁 = ( Hom ‘ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		fucbas.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuchom.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		eqid	⊢ ( 𝐶 Func 𝐷 ) = ( 𝐶 Func 𝐷 )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
6		simpl	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐶 ∈ Cat )
7		simpr	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
8		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
9	1 3 2 4 5 6 7 8	fuccofval	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( comp ‘ 𝑄 ) = ( 𝑣 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
10	1 3 2 4 5 6 7 9	fucval	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑄 = { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ } )
11		catstr	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ } Struct ⟨ 1 , ; 1 5 ⟩
12		homid	⊢ Hom = Slot ( Hom ‘ ndx )
13		snsstp2	⊢ { ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ }
14	2	ovexi	⊢ 𝑁 ∈ V
15	14	a1i	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑁 ∈ V )
16		eqid	⊢ ( Hom ‘ 𝑄 ) = ( Hom ‘ 𝑄 )
17	10 11 12 13 15 16	strfv3	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( Hom ‘ 𝑄 ) = 𝑁 )
18	17	eqcomd	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑁 = ( Hom ‘ 𝑄 ) )
19	12	str0	⊢ ∅ = ( Hom ‘ ∅ )
20	2	natffn	⊢ 𝑁 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) )
21		funcrcl	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
22	21	con3i	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ¬ 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
23	22	eq0rdv	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) = ∅ )
24	23	xpeq2d	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐶 Func 𝐷 ) × ∅ ) )
25		xp0	⊢ ( ( 𝐶 Func 𝐷 ) × ∅ ) = ∅
26	24 25	eqtrdi	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) = ∅ )
27	26	fneq2d	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝑁 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ↔ 𝑁 Fn ∅ ) )
28	20 27	mpbii	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑁 Fn ∅ )
29		fn0	⊢ ( 𝑁 Fn ∅ ↔ 𝑁 = ∅ )
30	28 29	sylib	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑁 = ∅ )
31		fnfuc	⊢ FuncCat Fn ( Cat × Cat )
32	31	fndmi	⊢ dom FuncCat = ( Cat × Cat )
33	32	ndmov	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 FuncCat 𝐷 ) = ∅ )
34	1 33	eqtrid	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑄 = ∅ )
35	34	fveq2d	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( Hom ‘ 𝑄 ) = ( Hom ‘ ∅ ) )
36	19 30 35	3eqtr4a	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑁 = ( Hom ‘ 𝑄 ) )
37	18 36	pm2.61i	⊢ 𝑁 = ( Hom ‘ 𝑄 )