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	⊢ 1 = ( SetCat ‘ 1o )
	funcsetc1o.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
	funcsetc1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion	funcsetc1ocl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1o )
2		funcsetc1o.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
3		funcsetc1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		eqid	⊢ ( 1 Δfunc 𝐶 ) = ( 1 Δfunc 𝐶 )
5		setc1oterm	⊢ ( SetCat ‘ 1o ) ∈ TermCat
6	1 5	eqeltri	⊢ 1 ∈ TermCat
7	6	a1i	⊢ ( 𝜑 → 1 ∈ TermCat )
8	7	termccd	⊢ ( 𝜑 → 1 ∈ Cat )
9	1	setc1obas	⊢ 1o = ( Base ‘ 1 )
10		0lt1o	⊢ ∅ ∈ 1o
11	10	a1i	⊢ ( 𝜑 → ∅ ∈ 1o )
12	4 8 3 9 11 2	diag1cl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )