Theorem incat

Description: Constructing a category with at most one object and at most two morphisms. If X is a set then C is the category A in Exercise 3G of Adamek p. 45. (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	incat.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , { 𝑋 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } ⟩ }
	incat.h	⊢ 𝐻 = { 𝐹 , 𝐺 }
	incat.x	⊢ · = ( 𝑓 ∈ 𝐻 , 𝑔 ∈ 𝐻 ↦ ( 𝑓 ∩ 𝑔 ) )
Assertion	incat	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { 𝑋 } ↦ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		incat.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , { 𝑋 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } ⟩ }
2		incat.h	⊢ 𝐻 = { 𝐹 , 𝐺 }
3		incat.x	⊢ · = ( 𝑓 ∈ 𝐻 , 𝑔 ∈ 𝐻 ↦ ( 𝑓 ∩ 𝑔 ) )
4		snex	⊢ { 𝑋 } ∈ V
5	1 4	catbas	⊢ { 𝑋 } = ( Base ‘ 𝐶 )
6	5	a1i	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → { 𝑋 } = ( Base ‘ 𝐶 ) )
7		snex	⊢ { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } ∈ V
8	1 7	cathomfval	⊢ { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } = ( Hom ‘ 𝐶 )
9	8	a1i	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } = ( Hom ‘ 𝐶 ) )
10		snex	⊢ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } ∈ V
11	1 10	catcofval	⊢ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } = ( comp ‘ 𝐶 )
12	11	a1i	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } = ( comp ‘ 𝐶 ) )
13		prex	⊢ { 𝐹 , 𝐺 } ∈ V
14	2 13	eqeltri	⊢ 𝐻 ∈ V
15	14	ovsn2	⊢ ( 𝑋 { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } 𝑋 ) = 𝐻
16	15 2	eqtri	⊢ ( 𝑋 { ⟨ 𝑋 , 𝑋 , 𝐻 ⟩ } 𝑋 ) = { 𝐹 , 𝐺 }
17	14 14	mpoex	⊢ ( 𝑓 ∈ 𝐻 , 𝑔 ∈ 𝐻 ↦ ( 𝑓 ∩ 𝑔 ) ) ∈ V
18	3 17	eqeltri	⊢ · ∈ V
19	18	ovsn2	⊢ ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) = ·
20	19 3	eqtri	⊢ ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) = ( 𝑓 ∈ 𝐻 , 𝑔 ∈ 𝐻 ↦ ( 𝑓 ∩ 𝑔 ) )
21	20	a1i	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) = ( 𝑓 ∈ 𝐻 , 𝑔 ∈ 𝐻 ↦ ( 𝑓 ∩ 𝑔 ) ) )
22		ineq12	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∩ 𝑔 ) = ( 𝐺 ∩ 𝐺 ) )
23		inidm	⊢ ( 𝐺 ∩ 𝐺 ) = 𝐺
24	22 23	eqtrdi	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∩ 𝑔 ) = 𝐺 )
25	24	adantl	⊢ ( ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐺 ) ) → ( 𝑓 ∩ 𝑔 ) = 𝐺 )
26		prid2g	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ { 𝐹 , 𝐺 } )
27	26 2	eleqtrrdi	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ 𝐻 )
28	27	adantl	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → 𝐺 ∈ 𝐻 )
29	21 25 28 28 28	ovmpod	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) 𝐺 ) = 𝐺 )
30		ineq12	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐹 ) → ( 𝑓 ∩ 𝑔 ) = ( 𝐺 ∩ 𝐹 ) )
31		sseqin2	⊢ ( 𝐹 ⊆ 𝐺 ↔ ( 𝐺 ∩ 𝐹 ) = 𝐹 )
32	31	birani	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = 𝐹 )
33	30 32	sylan9eqr	⊢ ( ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( 𝑓 ∩ 𝑔 ) = 𝐹 )
34		ssexg	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → 𝐹 ∈ V )
35		prid1g	⊢ ( 𝐹 ∈ V → 𝐹 ∈ { 𝐹 , 𝐺 } )
36	34 35	syl	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → 𝐹 ∈ { 𝐹 , 𝐺 } )
37	36 2	eleqtrrdi	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → 𝐹 ∈ 𝐻 )
38	21 33 28 37 37	ovmpod	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) 𝐹 ) = 𝐹 )
39		ineq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∩ 𝑔 ) = ( 𝐹 ∩ 𝐺 ) )
40		dfss2	⊢ ( 𝐹 ⊆ 𝐺 ↔ ( 𝐹 ∩ 𝐺 ) = 𝐹 )
41	40	birani	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 ∩ 𝐺 ) = 𝐹 )
42	39 41	sylan9eqr	⊢ ( ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑓 ∩ 𝑔 ) = 𝐹 )
43	21 42 37 28 37	ovmpod	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) 𝐺 ) = 𝐹 )
44		ineq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐹 ) → ( 𝑓 ∩ 𝑔 ) = ( 𝐹 ∩ 𝐹 ) )
45		inidm	⊢ ( 𝐹 ∩ 𝐹 ) = 𝐹
46	44 45	eqtrdi	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐹 ) → ( 𝑓 ∩ 𝑔 ) = 𝐹 )
47	46	adantl	⊢ ( ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐹 ) ) → ( 𝑓 ∩ 𝑔 ) = 𝐹 )
48	21 47 37 37 37	ovmpod	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) 𝐹 ) = 𝐹 )
49	48 36	eqeltrd	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ { ⟨ ⟨ 𝑋 , 𝑋 ⟩ , 𝑋 , · ⟩ } 𝑋 ) 𝐹 ) ∈ { 𝐹 , 𝐺 } )
50	6 9 12 16 29 38 43 49	2arwcat	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { 𝑋 } ↦ 𝐺 ) ) )