Theorem diag2f1lem

Description: Lemma for diag2f1 . The converse is trivial ( fveq2 ). (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag2f1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	diag2f1.a	$$⊢A={\mathrm{Base}}_C$$
	diag2f1.b	$$⊢B={\mathrm{Base}}_D$$
	diag2f1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	diag2f1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diag2f1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag2f1.x	$$⊢\phi \to X\in A$$
	diag2f1.y	$$⊢\phi \to Y\in A$$
	diag2f1.0	$$⊢\phi \to B\ne \varnothing$$
	diag2f1lem.f	$$⊢\phi \to F\in \left(XHY\right)$$
	diag2f1lem.g	$$⊢\phi \to G\in \left(XHY\right)$$
Assertion	diag2f1lem	$$⊢\phi \to \left(\left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(L\right)Y\right)\left(G\right)\to F=G\right)$$

Proof

Step	Hyp	Ref	Expression
1		diag2f1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diag2f1.a	$$⊢A={\mathrm{Base}}_C$$
3		diag2f1.b	$$⊢B={\mathrm{Base}}_D$$
4		diag2f1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		diag2f1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		diag2f1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
7		diag2f1.x	$$⊢\phi \to X\in A$$
8		diag2f1.y	$$⊢\phi \to Y\in A$$
9		diag2f1.0	$$⊢\phi \to B\ne \varnothing$$
10		diag2f1lem.f	$$⊢\phi \to F\in \left(XHY\right)$$
11		diag2f1lem.g	$$⊢\phi \to G\in \left(XHY\right)$$
12	1 2 3 4 5 6 7 8 10	diag2	$$⊢\phi \to \left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=B\times \left\{F\right\}$$
13	1 2 3 4 5 6 7 8 11	diag2	$$⊢\phi \to \left(X{2}^{nd}\left(L\right)Y\right)\left(G\right)=B\times \left\{G\right\}$$
14	12 13	eqeq12d	$$⊢\phi \to \left(\left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(L\right)Y\right)\left(G\right)\leftrightarrow B\times \left\{F\right\}=B\times \left\{G\right\}\right)$$
15		xpcan	$$⊢B\ne \varnothing \to \left(B\times \left\{F\right\}=B\times \left\{G\right\}\leftrightarrow \left\{F\right\}=\left\{G\right\}\right)$$
16	9 15	syl	$$⊢\phi \to \left(B\times \left\{F\right\}=B\times \left\{G\right\}\leftrightarrow \left\{F\right\}=\left\{G\right\}\right)$$
17	14 16	bitrd	$$⊢\phi \to \left(\left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(L\right)Y\right)\left(G\right)\leftrightarrow \left\{F\right\}=\left\{G\right\}\right)$$
18		sneqrg	$$⊢F\in \left(XHY\right)\to \left(\left\{F\right\}=\left\{G\right\}\to F=G\right)$$
19	10 18	syl	$$⊢\phi \to \left(\left\{F\right\}=\left\{G\right\}\to F=G\right)$$
20	17 19	sylbid	$$⊢\phi \to \left(\left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(L\right)Y\right)\left(G\right)\to F=G\right)$$