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	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
	funcsetc1o.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)$$
	funcsetc1o.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	funcsetc1o.b	$$⊢B={\mathrm{Base}}_C$$
	funcsetc1o.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	funcsetc1o	$$⊢\phi \to F=⟨B\times 1_{𝑜},\left(x\in B,y\in B⟼\left(xHy\right)\times 1_{𝑜}\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		funcsetc1o.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)$$
3		funcsetc1o.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		funcsetc1o.b	$$⊢B={\mathrm{Base}}_C$$
5		funcsetc1o.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
6		eqid	$$⊢\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C=\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C$$
7		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
8	1 7	eqeltri	Could not format .1. e. TermCat : No typesetting found for |- .1. e. TermCat with typecode |-
9	8	a1i	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
10	9	termccatd	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{Cat}$$
11	1	setc1obas	$$⊢1_{𝑜}={\mathrm{Base}}_{\underset{\dot{}}{1}}$$
12		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
13	12	a1i	$$⊢\phi \to \varnothing \in 1_{𝑜}$$
14		eqid	$$⊢\mathrm{Id}\left(\underset{\dot{}}{1}\right)=\mathrm{Id}\left(\underset{\dot{}}{1}\right)$$
15	6 10 3 11 13 2 4 5 14	diag1a	$$⊢\phi \to F=⟨B\times \left\{\varnothing \right\},\left(x\in B,y\in B⟼\left(xHy\right)\times \left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}\right)⟩$$
16		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
17	16	xpeq2i	$$⊢B\times 1_{𝑜}=B\times \left\{\varnothing \right\}$$
18	1 14	setc1oid	$$⊢\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)=\varnothing$$
19	18	sneqi	$$⊢\left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}=\left\{\varnothing \right\}$$
20	16 19	eqtr4i	$$⊢1_{𝑜}=\left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}$$
21	20	xpeq2i	$$⊢\left(xHy\right)\times 1_{𝑜}=\left(xHy\right)\times \left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}$$
22	21	a1i	$$⊢\left(x\in B\wedge y\in B\right)\to \left(xHy\right)\times 1_{𝑜}=\left(xHy\right)\times \left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}$$
23	22	mpoeq3ia	$$⊢\left(x\in B,y\in B⟼\left(xHy\right)\times 1_{𝑜}\right)=\left(x\in B,y\in B⟼\left(xHy\right)\times \left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}\right)$$
24	17 23	opeq12i	$$⊢⟨B\times 1_{𝑜},\left(x\in B,y\in B⟼\left(xHy\right)\times 1_{𝑜}\right)⟩=⟨B\times \left\{\varnothing \right\},\left(x\in B,y\in B⟼\left(xHy\right)\times \left\{\mathrm{Id}\left(\underset{\dot{}}{1}\right)\left(\varnothing \right)\right\}\right)⟩$$
25	15 24	eqtr4di	$$⊢\phi \to F=⟨B\times 1_{𝑜},\left(x\in B,y\in B⟼\left(xHy\right)\times 1_{𝑜}\right)⟩$$