diag2f1

Description: If B is non-empty, the morphism part of a diagonal functor is injective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag2f1.l	$⊢ L = C Δ_{func} D$
	diag2f1.a	$⊢ A = {Base}_{C}$
	diag2f1.b	$⊢ B = {Base}_{D}$
	diag2f1.h	$⊢ H = Hom (C)$
	diag2f1.c	$⊢ φ \to C \in Cat$
	diag2f1.d	$⊢ φ \to D \in Cat$
	diag2f1.x	$⊢ φ \to X \in A$
	diag2f1.y	$⊢ φ \to Y \in A$
	diag2f1.0	$⊢ φ \to B \neq \emptyset$
	diag2f1.n	$⊢ N = D Nat C$
Assertion	diag2f1	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$

Proof

Step	Hyp	Ref	Expression
1		diag2f1.l	$⊢ L = C Δ_{func} D$
2		diag2f1.a	$⊢ A = {Base}_{C}$
3		diag2f1.b	$⊢ B = {Base}_{D}$
4		diag2f1.h	$⊢ H = Hom (C)$
5		diag2f1.c	$⊢ φ \to C \in Cat$
6		diag2f1.d	$⊢ φ \to D \in Cat$
7		diag2f1.x	$⊢ φ \to X \in A$
8		diag2f1.y	$⊢ φ \to Y \in A$
9		diag2f1.0	$⊢ φ \to B \neq \emptyset$
10		diag2f1.n	$⊢ N = D Nat C$
11		eqid	$⊢ D FuncCat C = D FuncCat C$
12	11 10	fuchom	$⊢ N = Hom (D FuncCat C)$
13	1 5 6 11	diagcl	$⊢ φ \to L \in (C Func (D FuncCat C))$
14	13	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func (D FuncCat C)) 2^{nd} (L)$
15	2 4 12 14 7 8	funcf2	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y)$
16	5	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to C \in Cat$
17	6	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to D \in Cat$
18	7	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to X \in A$
19	8	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to Y \in A$
20	9	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to B \neq \emptyset$
21		simprl	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to f \in (X H Y)$
22		simprr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to g \in (X H Y)$
23	1 2 3 4 16 17 18 19 20 21 22	diag2f1lem	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to ((X 2^{nd} (L) Y) (f) = (X 2^{nd} (L) Y) (g) \to f = g)$
24	23	ralrimivva	$⊢ φ \to \forall f \in (X H Y) \forall g \in (X H Y) ((X 2^{nd} (L) Y) (f) = (X 2^{nd} (L) Y) (g) \to f = g)$
25		dff13	$⊢ (X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y) \leftrightarrow ((X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y) \land \forall f \in (X H Y) \forall g \in (X H Y) ((X 2^{nd} (L) Y) (f) = (X 2^{nd} (L) Y) (g) \to f = g))$
26	15 24 25	sylanbrc	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$

Metamath Proof Explorer

Theorem diag2f1

Proof