diag1f1

Description: The object part of the diagonal functor is 1-1 if B is non-empty. (Contributed by Zhi Wang, 19-Oct-2025)

Step	Hyp	Ref	Expression
1		diag1f1.l	$⊢ L = C Δ_{func} D$
2		diag1f1.c	$⊢ φ \to C \in Cat$
3		diag1f1.d	$⊢ φ \to D \in Cat$
4		diag1f1.a	$⊢ A = {Base}_{C}$
5		diag1f1.b	$⊢ B = {Base}_{D}$
6		diag1f1.0	$⊢ φ \to B \neq \emptyset$
7		eqid	$⊢ D FuncCat C = D FuncCat C$
8	7	fucbas	$⊢ D Func C = {Base}_{(D FuncCat C)}$
9	1 2 3 7	diagcl	$⊢ φ \to L \in (C Func (D FuncCat C))$
10	9	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func (D FuncCat C)) 2^{nd} (L)$
11	4 8 10	funcf1	$⊢ φ \to 1^{st} (L) : A ⟶ D Func C$
12	2	adantr	$⊢ (φ \land (x \in A \land y \in A)) \to C \in Cat$
13	3	adantr	$⊢ (φ \land (x \in A \land y \in A)) \to D \in Cat$
14	6	adantr	$⊢ (φ \land (x \in A \land y \in A)) \to B \neq \emptyset$
15		simprl	$⊢ (φ \land (x \in A \land y \in A)) \to x \in A$
16		simprr	$⊢ (φ \land (x \in A \land y \in A)) \to y \in A$
17		eqid	$⊢ 1^{st} (L) (x) = 1^{st} (L) (x)$
18		eqid	$⊢ 1^{st} (L) (y) = 1^{st} (L) (y)$
19	1 12 13 4 5 14 15 16 17 18	diag1f1lem	$⊢ (φ \land (x \in A \land y \in A)) \to (1^{st} (L) (x) = 1^{st} (L) (y) \to x = y)$
20	19	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in A (1^{st} (L) (x) = 1^{st} (L) (y) \to x = y)$
21		dff13	$⊢ 1^{st} (L) : A \underset{1-1}{⟶} D Func C \leftrightarrow (1^{st} (L) : A ⟶ D Func C \land \forall x \in A \forall y \in A (1^{st} (L) (x) = 1^{st} (L) (y) \to x = y))$
22	11 20 21	sylanbrc	$⊢ φ \to 1^{st} (L) : A \underset{1-1}{⟶} D Func C$

Metamath Proof Explorer