indthinc

Description: An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are (/) . This is a special case of prsthinc , where .<_ = ( B X. B ) . This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024) (Proof shortened by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Hypotheses	indthinc.b	$⊢ φ \to B = {Base}_{C}$
	indthinc.h	$⊢ φ \to (B \times B) \times \{1_{𝑜}\} = Hom (C)$
	indthinc.o	$⊢ φ \to \emptyset = comp (C)$
	indthinc.c	$⊢ φ \to C \in V$
Assertion	indthinc	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	$⊢ φ \to B = {Base}_{C}$
2		indthinc.h	$⊢ φ \to (B \times B) \times \{1_{𝑜}\} = Hom (C)$
3		indthinc.o	$⊢ φ \to \emptyset = comp (C)$
4		indthinc.c	$⊢ φ \to C \in V$
5		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to (B \times B) \times \{1_{𝑜}\} = (B \times B) \times \{1_{𝑜}\}$
6	5	f1omo	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in ((B \times B) \times \{1_{𝑜}\}) (⟨x, y⟩)$
7		df-ov	$⊢ x ((B \times B) \times \{1_{𝑜}\}) y = ((B \times B) \times \{1_{𝑜}\}) (⟨x, y⟩)$
8	7	eleq2i	$⊢ f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \leftrightarrow f \in ((B \times B) \times \{1_{𝑜}\}) (⟨x, y⟩)$
9	8	mobii	$⊢ \exists^{} f f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \leftrightarrow \exists^{} f f \in ((B \times B) \times \{1_{𝑜}\}) (⟨x, y⟩)$
10	6 9	sylibr	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x ((B \times B) \times \{1_{𝑜}\}) y)$
11		biid	$⊢ ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z))) \leftrightarrow ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z)))$
12		id	$⊢ y \in B \to y \in B$
13	12	ancli	$⊢ y \in B \to (y \in B \land y \in B)$
14		1oex	$⊢ 1_{𝑜} \in V$
15	14	ovconst2	$⊢ (y \in B \land y \in B) \to y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜}$
16		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
17		eleq2	$⊢ y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜} \to (\emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y) \leftrightarrow \emptyset \in 1_{𝑜})$
18	16 17	mpbiri	$⊢ y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜} \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
19	13 15 18	3syl	$⊢ y \in B \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
20	19	adantl	$⊢ (φ \land y \in B) \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
21	16	a1i	$⊢ (x \in B \land y \in B \land z \in B) \to \emptyset \in 1_{𝑜}$
22		0ov	$⊢ ⟨x, y⟩ \emptyset z = \emptyset$
23	22	oveqi	$⊢ g (⟨x, y⟩ \emptyset z) f = g \emptyset f$
24		0ov	$⊢ g \emptyset f = \emptyset$
25	23 24	eqtri	$⊢ g (⟨x, y⟩ \emptyset z) f = \emptyset$
26	25	a1i	$⊢ (x \in B \land y \in B \land z \in B) \to g (⟨x, y⟩ \emptyset z) f = \emptyset$
27	14	ovconst2	$⊢ (x \in B \land z \in B) \to x ((B \times B) \times \{1_{𝑜}\}) z = 1_{𝑜}$
28	27	3adant2	$⊢ (x \in B \land y \in B \land z \in B) \to x ((B \times B) \times \{1_{𝑜}\}) z = 1_{𝑜}$
29	21 26 28	3eltr4d	$⊢ (x \in B \land y \in B \land z \in B) \to g (⟨x, y⟩ \emptyset z) f \in (x ((B \times B) \times \{1_{𝑜}\}) z)$
30	29	ad2antrl	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z)))) \to g (⟨x, y⟩ \emptyset z) f \in (x ((B \times B) \times \{1_{𝑜}\}) z)$
31	1 2 10 3 4 11 20 30	isthincd2	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \emptyset))$

Metamath Proof Explorer

Theorem indthinc

Proof