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{˙}{1} = SetCat (1_{𝑜})$
	funcsetc1o.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (\emptyset)$
	funcsetc1o.c	$⊢ φ \to C \in Cat$
Assertion	funcsetc1ocl	$⊢ φ \to F \in (C Func \underset{˙}{1})$

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$⊢ \underset{˙}{1} = SetCat (1_{𝑜})$
2		funcsetc1o.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (\emptyset)$
3		funcsetc1o.c	$⊢ φ \to C \in Cat$
4		eqid	$⊢ \underset{˙}{1} Δ_{func} C = \underset{˙}{1} Δ_{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	$⊢ φ \to \underset{˙}{1} \in Cat$
9	1	setc1obas	$⊢ 1_{𝑜} = {Base}_{\underset{˙}{1}}$
10		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
11	10	a1i	$⊢ φ \to \emptyset \in 1_{𝑜}$
12	4 8 3 9 11 2	diag1cl	$⊢ φ \to F \in (C Func \underset{˙}{1})$

Metamath Proof Explorer