Theorem diagffth

Description: The diagonal functor is a fully faithful functor from a category C to the category of functors from a terminal category to C . (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diagffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
	diagffth.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
Assertion	diagffth	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
4		diagffth.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
5		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
6	2	termccd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
7	4 1 6 3	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) )
8		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝑄 ) ) → 𝐿 = ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ )
9	5 7 8	sylancr	⊢ ( 𝜑 → 𝐿 = ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ )
10	7	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐿 ) )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
14		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
15		eqid	⊢ ( 𝐷 Nat 𝐶 ) = ( 𝐷 Nat 𝐶 )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐷 ∈ TermCat )
17	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
18	4 11 12 13 14 15 16 17	diag2f1o	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) )
19	18	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) )
20	3 15	fuchom	⊢ ( 𝐷 Nat 𝐶 ) = ( Hom ‘ 𝑄 )
21	11 12 20	isffth2	⊢ ( ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) ↔ ( ( 1st ‘ 𝐿 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ) )
22	10 19 21	sylanbrc	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) )
23		df-br	⊢ ( ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) ↔ ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
24	22 23	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
25	9 24	eqeltrd	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )