Theorem termcfuncval

Description: The value of a functor from a terminal category. (Contributed by Zhi Wang, 20-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)$$
	termcfuncval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	termcfuncval.i	$$⊢I=\mathrm{Id}\left(D\right)$$
Assertion	termcfuncval	$$⊢\phi \to \left(X\in A\wedge K=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\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		termcfuncval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
8		termcfuncval.i	$$⊢I=\mathrm{Id}\left(D\right)$$
9	3	func1st2nd	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Func}C\right)2^{nd}\left(K\right)$$
10	4 1 9	funcf1	$$⊢\phi \to 1^{st}\left(K\right):B⟶A$$
11	10 5	ffvelcdmd	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)\in A$$
12	6 11	eqeltrid	$$⊢\phi \to X\in A$$
13		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}C\right)$$
14		1st2nd	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}C\right)\wedge K\in \left(D\mathrm{Func}C\right)\right)\to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
15	13 3 14	sylancr	$$⊢\phi \to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
16	2 4 5	termcbas2	$$⊢\phi \to B=\left\{Y\right\}$$
17	16	feq2d	$$⊢\phi \to \left(1^{st}\left(K\right):B⟶A\leftrightarrow 1^{st}\left(K\right):\left\{Y\right\}⟶A\right)$$
18	10 17	mpbid	$$⊢\phi \to 1^{st}\left(K\right):\left\{Y\right\}⟶A$$
19		fsn2g	$$⊢Y\in B\to \left(1^{st}\left(K\right):\left\{Y\right\}⟶A\leftrightarrow \left(1^{st}\left(K\right)\left(Y\right)\in A\wedge 1^{st}\left(K\right)=\left\{⟨Y,1^{st}\left(K\right)\left(Y\right)⟩\right\}\right)\right)$$
20	5 19	syl	$$⊢\phi \to \left(1^{st}\left(K\right):\left\{Y\right\}⟶A\leftrightarrow \left(1^{st}\left(K\right)\left(Y\right)\in A\wedge 1^{st}\left(K\right)=\left\{⟨Y,1^{st}\left(K\right)\left(Y\right)⟩\right\}\right)\right)$$
21	18 20	mpbid	$$⊢\phi \to \left(1^{st}\left(K\right)\left(Y\right)\in A\wedge 1^{st}\left(K\right)=\left\{⟨Y,1^{st}\left(K\right)\left(Y\right)⟩\right\}\right)$$
22	21	simprd	$$⊢\phi \to 1^{st}\left(K\right)=\left\{⟨Y,1^{st}\left(K\right)\left(Y\right)⟩\right\}$$
23	6	opeq2i	$$⊢⟨Y,X⟩=⟨Y,1^{st}\left(K\right)\left(Y\right)⟩$$
24	23	sneqi	$$⊢\left\{⟨Y,X⟩\right\}=\left\{⟨Y,1^{st}\left(K\right)\left(Y\right)⟩\right\}$$
25	22 24	eqtr4di	$$⊢\phi \to 1^{st}\left(K\right)=\left\{⟨Y,X⟩\right\}$$
26	4 9	funcfn2	$$⊢\phi \to 2^{nd}\left(K\right)Fn\left(B\times B\right)$$
27	16	sqxpeqd	$$⊢\phi \to B\times B=\left\{Y\right\}\times \left\{Y\right\}$$
28		xpsng	$$⊢\left(Y\in B\wedge Y\in B\right)\to \left\{Y\right\}\times \left\{Y\right\}=\left\{⟨Y,Y⟩\right\}$$
29	5 5 28	syl2anc	$$⊢\phi \to \left\{Y\right\}\times \left\{Y\right\}=\left\{⟨Y,Y⟩\right\}$$
30	27 29	eqtrd	$$⊢\phi \to B\times B=\left\{⟨Y,Y⟩\right\}$$
31	30	fneq2d	$$⊢\phi \to \left(2^{nd}\left(K\right)Fn\left(B\times B\right)\leftrightarrow 2^{nd}\left(K\right)Fn\left\{⟨Y,Y⟩\right\}\right)$$
32	26 31	mpbid	$$⊢\phi \to 2^{nd}\left(K\right)Fn\left\{⟨Y,Y⟩\right\}$$
33		opex	$$⊢⟨Y,Y⟩\in \mathrm{V}$$
34	33	fnsnb	$$⊢2^{nd}\left(K\right)Fn\left\{⟨Y,Y⟩\right\}\leftrightarrow 2^{nd}\left(K\right)=\left\{⟨⟨Y,Y⟩,2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)⟩\right\}$$
35	32 34	sylib	$$⊢\phi \to 2^{nd}\left(K\right)=\left\{⟨⟨Y,Y⟩,2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)⟩\right\}$$
36		df-ov	$$⊢Y{2}^{nd}\left(K\right)Y=2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)$$
37		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
38		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
39	4 37 38 9 5 5	funcf2	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Y\right):Y\mathrm{Hom}\left(D\right)Y⟶1^{st}\left(K\right)\left(Y\right)\mathrm{Hom}\left(C\right)1^{st}\left(K\right)\left(Y\right)$$
40	2 4 5 5 37 8	termchom	$$⊢\phi \to Y\mathrm{Hom}\left(D\right)Y=\left\{I\left(Y\right)\right\}$$
41	40	eqcomd	$$⊢\phi \to \left\{I\left(Y\right)\right\}=Y\mathrm{Hom}\left(D\right)Y$$
42	6 6	oveq12i	$$⊢X\mathrm{Hom}\left(C\right)X=1^{st}\left(K\right)\left(Y\right)\mathrm{Hom}\left(C\right)1^{st}\left(K\right)\left(Y\right)$$
43	42	a1i	$$⊢\phi \to X\mathrm{Hom}\left(C\right)X=1^{st}\left(K\right)\left(Y\right)\mathrm{Hom}\left(C\right)1^{st}\left(K\right)\left(Y\right)$$
44	41 43	feq23d	$$⊢\phi \to \left(\left(Y{2}^{nd}\left(K\right)Y\right):\left\{I\left(Y\right)\right\}⟶X\mathrm{Hom}\left(C\right)X\leftrightarrow \left(Y{2}^{nd}\left(K\right)Y\right):Y\mathrm{Hom}\left(D\right)Y⟶1^{st}\left(K\right)\left(Y\right)\mathrm{Hom}\left(C\right)1^{st}\left(K\right)\left(Y\right)\right)$$
45	39 44	mpbird	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Y\right):\left\{I\left(Y\right)\right\}⟶X\mathrm{Hom}\left(C\right)X$$
46		fvex	$$⊢I\left(Y\right)\in \mathrm{V}$$
47	46	fsn2	$$⊢\left(Y{2}^{nd}\left(K\right)Y\right):\left\{I\left(Y\right)\right\}⟶X\mathrm{Hom}\left(C\right)X\leftrightarrow \left(\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)\wedge Y{2}^{nd}\left(K\right)Y=\left\{⟨I\left(Y\right),\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)⟩\right\}\right)$$
48	45 47	sylib	$$⊢\phi \to \left(\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)\wedge Y{2}^{nd}\left(K\right)Y=\left\{⟨I\left(Y\right),\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)⟩\right\}\right)$$
49	48	simprd	$$⊢\phi \to Y{2}^{nd}\left(K\right)Y=\left\{⟨I\left(Y\right),\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)⟩\right\}$$
50	4 8 7 9 5	funcid	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)=\underset{\dot{}}{1}\left(1^{st}\left(K\right)\left(Y\right)\right)$$
51	6	fveq2i	$$⊢\underset{\dot{}}{1}\left(X\right)=\underset{\dot{}}{1}\left(1^{st}\left(K\right)\left(Y\right)\right)$$
52	50 51	eqtr4di	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)=\underset{\dot{}}{1}\left(X\right)$$
53	52	opeq2d	$$⊢\phi \to ⟨I\left(Y\right),\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)⟩=⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩$$
54	53	sneqd	$$⊢\phi \to \left\{⟨I\left(Y\right),\left(Y{2}^{nd}\left(K\right)Y\right)\left(I\left(Y\right)\right)⟩\right\}=\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}$$
55	49 54	eqtrd	$$⊢\phi \to Y{2}^{nd}\left(K\right)Y=\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}$$
56	36 55	eqtr3id	$$⊢\phi \to 2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)=\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}$$
57	56	opeq2d	$$⊢\phi \to ⟨⟨Y,Y⟩,2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)⟩=⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩$$
58	57	sneqd	$$⊢\phi \to \left\{⟨⟨Y,Y⟩,2^{nd}\left(K\right)\left(⟨Y,Y⟩\right)⟩\right\}=\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\right\}$$
59	35 58	eqtrd	$$⊢\phi \to 2^{nd}\left(K\right)=\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\right\}$$
60	25 59	opeq12d	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\right\}⟩$$
61	15 60	eqtrd	$$⊢\phi \to K=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\right\}⟩$$
62	12 61	jca	$$⊢\phi \to \left(X\in A\wedge K=⟨\left\{⟨Y,X⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨I\left(Y\right),\underset{\dot{}}{1}\left(X\right)⟩\right\}⟩\right\}⟩\right)$$