Theorem functermc2

Description: Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	functermc.d	|- ( ph -> D e. Cat )
	functermc.e	|- ( ph -> E e. TermCat )
	functermc.b	|- B = ( Base ` D )
	functermc.c	|- C = ( Base ` E )
	functermc.h	|- H = ( Hom ` D )
	functermc.j	|- J = ( Hom ` E )
	functermc.f	|- F = ( B X. C )
	functermc.g	|- G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
Assertion	functermc2	|- ( ph -> ( D Func E ) = { <. F , G >. } )

Proof

Step	Hyp	Ref	Expression
1		functermc.d	|- ( ph -> D e. Cat )
2		functermc.e	|- ( ph -> E e. TermCat )
3		functermc.b	|- B = ( Base ` D )
4		functermc.c	|- C = ( Base ` E )
5		functermc.h	|- H = ( Hom ` D )
6		functermc.j	|- J = ( Hom ` E )
7		functermc.f	|- F = ( B X. C )
8		functermc.g	|- G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
9		relfunc	|- Rel ( D Func E )
10	3	fvexi	|- B e. _V
11	4	fvexi	|- C e. _V
12	10 11	xpex	|- ( B X. C ) e. _V
13	7 12	eqeltri	|- F e. _V
14	10 10	mpoex	|- ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) e. _V
15	8 14	eqeltri	|- G e. _V
16	13 15	relsnop	|- Rel { <. F , G >. }
17	1 2 3 4 5 6 7 8	functermc	|- ( ph -> ( z ( D Func E ) w <-> ( z = F /\ w = G ) ) )
18		brsnop	|- ( ( F e. _V /\ G e. _V ) -> ( z { <. F , G >. } w <-> ( z = F /\ w = G ) ) )
19	13 15 18	mp2an	|- ( z { <. F , G >. } w <-> ( z = F /\ w = G ) )
20	17 19	bitr4di	|- ( ph -> ( z ( D Func E ) w <-> z { <. F , G >. } w ) )
21	9 16 20	eqbrrdiv	|- ( ph -> ( D Func E ) = { <. F , G >. } )