Theorem funcsetc1ocl

Description: The functor to the trivial category. The converse is also true due to reverse closure. (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}$$
Assertion	funcsetc1ocl	$$⊢\phi \to F\in \left(C\mathrm{Func}\underset{\dot{}}{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		eqid	$$⊢\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C=\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C$$
5		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
6	1 5	eqeltri	Could not format .1. e. TermCat : No typesetting found for |- .1. e. TermCat with typecode |-
7	6	a1i	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
8	7	termccd	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{Cat}$$
9	1	setc1obas	$$⊢1_{𝑜}={\mathrm{Base}}_{\underset{\dot{}}{1}}$$
10		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
11	10	a1i	$$⊢\phi \to \varnothing \in 1_{𝑜}$$
12	4 8 3 9 11 2	diag1cl	$$⊢\phi \to F\in \left(C\mathrm{Func}\underset{\dot{}}{1}\right)$$