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	$⊢ φ \to C \in Cat$
	diagffth.d	No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
	diagffth.q	$⊢ Q = D FuncCat C$
	diagffth.l	$⊢ L = C Δ_{func} D$
Assertion	diagffth	$⊢ φ \to L \in ((C Full Q) \cap (C Faith Q))$

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	$⊢ φ \to C \in Cat$
2		diagffth.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
3		diagffth.q	$⊢ Q = D FuncCat C$
4		diagffth.l	$⊢ L = C Δ_{func} D$
5		relfunc	$⊢ Rel (C Func Q)$
6	2	termccatd	$⊢ φ \to D \in Cat$
7	4 1 6 3	diagcl	$⊢ φ \to L \in (C Func Q)$
8		1st2nd	$⊢ (Rel (C Func Q) \land L \in (C Func Q)) \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
9	5 7 8	sylancr	$⊢ φ \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
10	7	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func Q) 2^{nd} (L)$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12		eqid	$⊢ Hom (C) = Hom (C)$
13		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
14		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
15		eqid	$⊢ D Nat C = D Nat C$
16	2	adantr	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> D e. TermCat ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> D e. TermCat ) with typecode \|-
17	1	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to C \in Cat$
18	4 11 12 13 14 15 16 17	diag2f1o	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (L) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (L) (x) (D Nat C) 1^{st} (L) (y)$
19	18	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (L) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (L) (x) (D Nat C) 1^{st} (L) (y)$
20	3 15	fuchom	$⊢ D Nat C = Hom (Q)$
21	11 12 20	isffth2	$⊢ 1^{st} (L) ((C Full Q) \cap (C Faith Q)) 2^{nd} (L) \leftrightarrow (1^{st} (L) (C Func Q) 2^{nd} (L) \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (L) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (L) (x) (D Nat C) 1^{st} (L) (y))$
22	10 19 21	sylanbrc	$⊢ φ \to 1^{st} (L) ((C Full Q) \cap (C Faith Q)) 2^{nd} (L)$
23		df-br	$⊢ 1^{st} (L) ((C Full Q) \cap (C Faith Q)) 2^{nd} (L) \leftrightarrow ⟨1^{st} (L), 2^{nd} (L)⟩ \in ((C Full Q) \cap (C Faith Q))$
24	22 23	sylib	$⊢ φ \to ⟨1^{st} (L), 2^{nd} (L)⟩ \in ((C Full Q) \cap (C Faith Q))$
25	9 24	eqeltrd	$⊢ φ \to L \in ((C Full Q) \cap (C Faith Q))$

Metamath Proof Explorer

Theorem diagffth

Proof