Theorem diag1f1lem

Description: The object part of the diagonal functor is 1-1 if B is non-empty. Note that ( ph -> ( M = N <-> X = Y ) ) also holds because of diag1f1 and f1fveq . (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	diag1f1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diag1f1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag1f1.a	$$⊢A={\mathrm{Base}}_C$$
	diag1f1.b	$$⊢B={\mathrm{Base}}_D$$
	diag1f1.0	$$⊢\phi \to B\ne \varnothing$$
	diag1f1lem.x	$$⊢\phi \to X\in A$$
	diag1f1lem.y	$$⊢\phi \to Y\in A$$
	diag1f1lem.m	$$⊢M=1^{st}\left(L\right)\left(X\right)$$
	diag1f1lem.n	$$⊢N=1^{st}\left(L\right)\left(Y\right)$$
Assertion	diag1f1lem	$$⊢\phi \to \left(M=N\to X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		diag1f1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diag1f1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		diag1f1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		diag1f1.a	$$⊢A={\mathrm{Base}}_C$$
5		diag1f1.b	$$⊢B={\mathrm{Base}}_D$$
6		diag1f1.0	$$⊢\phi \to B\ne \varnothing$$
7		diag1f1lem.x	$$⊢\phi \to X\in A$$
8		diag1f1lem.y	$$⊢\phi \to Y\in A$$
9		diag1f1lem.m	$$⊢M=1^{st}\left(L\right)\left(X\right)$$
10		diag1f1lem.n	$$⊢N=1^{st}\left(L\right)\left(Y\right)$$
11		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
12		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
13	1 2 3 4 7 9 5 11 12	diag1a	$$⊢\phi \to M=⟨B\times \left\{X\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩$$
14	1 2 3 4 8 10 5 11 12	diag1a	$$⊢\phi \to N=⟨B\times \left\{Y\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(Y\right)\right\}\right)⟩$$
15	13 14	eqeq12d	$$⊢\phi \to \left(M=N\leftrightarrow ⟨B\times \left\{X\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩=⟨B\times \left\{Y\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(Y\right)\right\}\right)⟩\right)$$
16	5	fvexi	$$⊢B\in \mathrm{V}$$
17		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
18	16 17	xpex	$$⊢B\times \left\{X\right\}\in \mathrm{V}$$
19	16 16	mpoex	$$⊢\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)\in \mathrm{V}$$
20	18 19	opth1	$$⊢⟨B\times \left\{X\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩=⟨B\times \left\{Y\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(Y\right)\right\}\right)⟩\to B\times \left\{X\right\}=B\times \left\{Y\right\}$$
21		xpcan	$$⊢B\ne \varnothing \to \left(B\times \left\{X\right\}=B\times \left\{Y\right\}\leftrightarrow \left\{X\right\}=\left\{Y\right\}\right)$$
22	6 21	syl	$$⊢\phi \to \left(B\times \left\{X\right\}=B\times \left\{Y\right\}\leftrightarrow \left\{X\right\}=\left\{Y\right\}\right)$$
23		sneqrg	$$⊢X\in A\to \left(\left\{X\right\}=\left\{Y\right\}\to X=Y\right)$$
24	7 23	syl	$$⊢\phi \to \left(\left\{X\right\}=\left\{Y\right\}\to X=Y\right)$$
25	22 24	sylbid	$$⊢\phi \to \left(B\times \left\{X\right\}=B\times \left\{Y\right\}\to X=Y\right)$$
26	20 25	syl5	$$⊢\phi \to \left(⟨B\times \left\{X\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩=⟨B\times \left\{Y\right\},\left(x\in B,y\in B⟼\left(x\mathrm{Hom}\left(D\right)y\right)\times \left\{\mathrm{Id}\left(C\right)\left(Y\right)\right\}\right)⟩\to X=Y\right)$$
27	15 26	sylbid	$$⊢\phi \to \left(M=N\to X=Y\right)$$