Theorem funcsetc1o

Description: Value of the functor to the trivial category. The converse is also true because F would be the empty set if C were not a category; and the empty set cannot equal an ordered pair of two sets. (Contributed by Zhi Wang, 22-Oct-2025)

	Ref	Expression
Hypotheses	funcsetc1o.1	|- .1. = ( SetCat ` 1o )
	funcsetc1o.f	|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
	funcsetc1o.c	|- ( ph -> C e. Cat )
	funcsetc1o.b	|- B = ( Base ` C )
	funcsetc1o.h	|- H = ( Hom ` C )
Assertion	funcsetc1o	|- ( ph -> F = <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. )

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	|- .1. = ( SetCat ` 1o )
2		funcsetc1o.f	|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
3		funcsetc1o.c	|- ( ph -> C e. Cat )
4		funcsetc1o.b	|- B = ( Base ` C )
5		funcsetc1o.h	|- H = ( Hom ` C )
6		eqid	|- ( .1. DiagFunc C ) = ( .1. DiagFunc C )
7		setc1oterm	|- ( SetCat ` 1o ) e. TermCat
8	1 7	eqeltri	|- .1. e. TermCat
9	8	a1i	|- ( ph -> .1. e. TermCat )
10	9	termccd	|- ( ph -> .1. e. Cat )
11	1	setc1obas	|- 1o = ( Base ` .1. )
12		0lt1o	|- (/) e. 1o
13	12	a1i	|- ( ph -> (/) e. 1o )
14		eqid	|- ( Id ` .1. ) = ( Id ` .1. )
15	6 10 3 11 13 2 4 5 14	diag1a	|- ( ph -> F = <. ( B X. { (/) } ) , ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) ) >. )
16		df1o2	|- 1o = { (/) }
17	16	xpeq2i	|- ( B X. 1o ) = ( B X. { (/) } )
18	1 14	setc1oid	|- ( ( Id ` .1. ) ` (/) ) = (/)
19	18	sneqi	|- { ( ( Id ` .1. ) ` (/) ) } = { (/) }
20	16 19	eqtr4i	|- 1o = { ( ( Id ` .1. ) ` (/) ) }
21	20	xpeq2i	|- ( ( x H y ) X. 1o ) = ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } )
22	21	a1i	|- ( ( x e. B /\ y e. B ) -> ( ( x H y ) X. 1o ) = ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) )
23	22	mpoeq3ia	|- ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) = ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) )
24	17 23	opeq12i	|- <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. = <. ( B X. { (/) } ) , ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) ) >.
25	15 24	eqtr4di	|- ( ph -> F = <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. )