Theorem 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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	indthinc.h	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
	indthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
	indthinc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion	indthinc	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2		indthinc.h	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
3		indthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
4		indthinc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( ( 𝐵 × 𝐵 ) × { 1o } ) )
6	5	f1omo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
7		df-ov	⊢ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
8	7	eleq2i	⊢ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
9	8	mobii	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
10	6 9	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
11		biid	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) )
12		id	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 )
13	12	ancli	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
14		1oex	⊢ 1o ∈ V
15	14	ovconst2	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o )
16		0lt1o	⊢ ∅ ∈ 1o
17		eleq2	⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ( ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ∅ ∈ 1o ) )
18	16 17	mpbiri	⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
19	13 15 18	3syl	⊢ ( 𝑦 ∈ 𝐵 → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
21	16	a1i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ∅ ∈ 1o )
22		0ov	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) = ∅
23	22	oveqi	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ( 𝑔 ∅ 𝑓 )
24		0ov	⊢ ( 𝑔 ∅ 𝑓 ) = ∅
25	23 24	eqtri	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅
26	25	a1i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅ )
27	14	ovconst2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
28	27	3adant2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
29	21 26 28	3eltr4d	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
30	29	ad2antrl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
31	1 2 10 3 4 11 20 30	isthincd2	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )