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{˙}{1} = SetCat (1_{𝑜})$
	funcsetc1o.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (\emptyset)$
	funcsetc1o.c	$⊢ φ \to C \in Cat$
	funcsetc1o.b	$⊢ B = {Base}_{C}$
	funcsetc1o.h	$⊢ H = Hom (C)$
Assertion	funcsetc1o	$⊢ φ \to F = ⟨B \times 1_{𝑜}, (x \in B, y \in B ⟼ (x H y) \times 1_{𝑜})⟩$

Proof

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		funcsetc1o.b	$⊢ B = {Base}_{C}$
5		funcsetc1o.h	$⊢ H = Hom (C)$
6		eqid	$⊢ \underset{˙}{1} Δ_{func} C = \underset{˙}{1} Δ_{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	termccd	$⊢ φ \to \underset{˙}{1} \in Cat$
11	1	setc1obas	$⊢ 1_{𝑜} = {Base}_{\underset{˙}{1}}$
12		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
13	12	a1i	$⊢ φ \to \emptyset \in 1_{𝑜}$
14		eqid	$⊢ Id (\underset{˙}{1}) = Id (\underset{˙}{1})$
15	6 10 3 11 13 2 4 5 14	diag1a	$⊢ φ \to F = ⟨B \times \{\emptyset\}, (x \in B, y \in B ⟼ (x H y) \times \{Id (\underset{˙}{1}) (\emptyset)\})⟩$
16		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
17	16	xpeq2i	$⊢ B \times 1_{𝑜} = B \times \{\emptyset\}$
18	1 14	setc1oid	$⊢ Id (\underset{˙}{1}) (\emptyset) = \emptyset$
19	18	sneqi	$⊢ \{Id (\underset{˙}{1}) (\emptyset)\} = \{\emptyset\}$
20	16 19	eqtr4i	$⊢ 1_{𝑜} = \{Id (\underset{˙}{1}) (\emptyset)\}$
21	20	xpeq2i	$⊢ (x H y) \times 1_{𝑜} = (x H y) \times \{Id (\underset{˙}{1}) (\emptyset)\}$
22	21	a1i	$⊢ (x \in B \land y \in B) \to (x H y) \times 1_{𝑜} = (x H y) \times \{Id (\underset{˙}{1}) (\emptyset)\}$
23	22	mpoeq3ia	$⊢ (x \in B, y \in B ⟼ (x H y) \times 1_{𝑜}) = (x \in B, y \in B ⟼ (x H y) \times \{Id (\underset{˙}{1}) (\emptyset)\})$
24	17 23	opeq12i	$⊢ ⟨B \times 1_{𝑜}, (x \in B, y \in B ⟼ (x H y) \times 1_{𝑜})⟩ = ⟨B \times \{\emptyset\}, (x \in B, y \in B ⟼ (x H y) \times \{Id (\underset{˙}{1}) (\emptyset)\})⟩$
25	15 24	eqtr4di	$⊢ φ \to F = ⟨B \times 1_{𝑜}, (x \in B, y \in B ⟼ (x H y) \times 1_{𝑜})⟩$

Metamath Proof Explorer

Theorem funcsetc1o

Proof