Theorem diag1f1olem

Description: To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1o.a	$$⊢A={\mathrm{Base}}_C$$
	diag1f1o.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
	termcfuncval.k	$$⊢\phi \to K\in \left(D\mathrm{Func}C\right)$$
	termcfuncval.b	$$⊢B={\mathrm{Base}}_D$$
	termcfuncval.y	$$⊢\phi \to Y\in B$$
	termcfuncval.x	$$⊢X=1^{st}\left(K\right)\left(Y\right)$$
	diag1f1olem.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
Assertion	diag1f1olem	$$⊢\phi \to \left(X\in A\wedge K=1^{st}\left(L\right)\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		diag1f1o.a	$$⊢A={\mathrm{Base}}_C$$
2		diag1f1o.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
3		termcfuncval.k	$$⊢\phi \to K\in \left(D\mathrm{Func}C\right)$$
4		termcfuncval.b	$$⊢B={\mathrm{Base}}_D$$
5		termcfuncval.y	$$⊢\phi \to Y\in B$$
6		termcfuncval.x	$$⊢X=1^{st}\left(K\right)\left(Y\right)$$
7		diag1f1olem.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
8		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
9		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
10	1 2 3 4 5 6 8 9	termcfuncval	$$⊢\phi \to \left(X\in A\wedge K=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}⟩\right)$$
11	10	simpld	$$⊢\phi \to X\in A$$
12	2 4 5	termcbas2	$$⊢\phi \to B=\left\{Y\right\}$$
13	12	xpeq1d	$$⊢\phi \to B\times \left\{X\right\}=\left\{Y\right\}\times \left\{X\right\}$$
14		xpsng	$$⊢\left(Y\in B\wedge X\in A\right)\to \left\{Y\right\}\times \left\{X\right\}=\left\{⟨Y,X⟩\right\}$$
15	5 11 14	syl2anc	$$⊢\phi \to \left\{Y\right\}\times \left\{X\right\}=\left\{⟨Y,X⟩\right\}$$
16	13 15	eqtrd	$$⊢\phi \to B\times \left\{X\right\}=\left\{⟨Y,X⟩\right\}$$
17	12	adantr	$$⊢\left(\phi \wedge y\in B\right)\to B=\left\{Y\right\}$$
18	2	adantr	Could not format ( ( ph /\ ( y e. B /\ z e. B ) ) -> D e. TermCat ) : No typesetting found for |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> D e. TermCat ) with typecode |-
19		simprl	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to y\in B$$
20		simprr	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to z\in B$$
21		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
22	5	adantr	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to Y\in B$$
23	18 4 19 20 21 9 22	termchom2	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to y\mathrm{Hom}\left(D\right)z=\left\{\mathrm{Id}\left(D\right)\left(Y\right)\right\}$$
24	23	xpeq1d	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to \left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}=\left\{\mathrm{Id}\left(D\right)\left(Y\right)\right\}\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}$$
25		fvex	$$⊢\mathrm{Id}\left(D\right)\left(Y\right)\in \mathrm{V}$$
26		fvex	$$⊢\mathrm{Id}\left(C\right)\left(X\right)\in \mathrm{V}$$
27	25 26	xpsn	$$⊢\left\{\mathrm{Id}\left(D\right)\left(Y\right)\right\}\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}=\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}$$
28	24 27	eqtrdi	$$⊢\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\to \left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}=\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}$$
29	12 17 28	mpoeq123dva	$$⊢\phi \to \left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)=\left(y\in \left\{Y\right\},z\in \left\{Y\right\}⟼\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\right)$$
30		snex	$$⊢\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\in \mathrm{V}$$
31	30	a1i	$$⊢\phi \to \left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\in \mathrm{V}$$
32		eqid	$$⊢\left(y\in \left\{Y\right\},z\in \left\{Y\right\}⟼\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\right)=\left(y\in \left\{Y\right\},z\in \left\{Y\right\}⟼\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\right)$$
33		eqidd	$$⊢y=Y\to \left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}=\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}$$
34		eqidd	$$⊢z=Y\to \left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}=\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}$$
35	32 33 34	mposn	$$⊢\left(Y\in B\wedge Y\in B\wedge \left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\in \mathrm{V}\right)\to \left(y\in \left\{Y\right\},z\in \left\{Y\right\}⟼\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\right)=\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}$$
36	5 5 31 35	syl3anc	$$⊢\phi \to \left(y\in \left\{Y\right\},z\in \left\{Y\right\}⟼\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}\right)=\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}$$
37	29 36	eqtrd	$$⊢\phi \to \left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)=\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}$$
38	16 37	opeq12d	$$⊢\phi \to ⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}⟩$$
39	3	func1st2nd	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Func}C\right)2^{nd}\left(K\right)$$
40	39	funcrcl3	$$⊢\phi \to C\in \mathrm{Cat}$$
41	2	termccd	$$⊢\phi \to D\in \mathrm{Cat}$$
42		eqid	$$⊢1^{st}\left(L\right)\left(X\right)=1^{st}\left(L\right)\left(X\right)$$
43	7 40 41 1 11 42 4 21 8	diag1a	$$⊢\phi \to 1^{st}\left(L\right)\left(X\right)=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(D\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩$$
44	10	simprd	$$⊢\phi \to K=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩\right\}⟩\right\}⟩$$
45	38 43 44	3eqtr4rd	$$⊢\phi \to K=1^{st}\left(L\right)\left(X\right)$$
46	11 45	jca	$$⊢\phi \to \left(X\in A\wedge K=1^{st}\left(L\right)\left(X\right)\right)$$