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	$$⊢C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{X\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨X,X,H⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}⟩\right\}$$
	incat.h	$$⊢H=\left\{F,G\right\}$$
	incat.x	$$⊢\underset{\dot{}}{·}=\left(f\in H,g\in H⟼f\cap g\right)$$
Assertion	incat	$$⊢\left(F\subseteq G\wedge G\in V\right)\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(y\in \left\{X\right\}⟼G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		incat.c	$$⊢C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{X\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨X,X,H⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}⟩\right\}$$
2		incat.h	$$⊢H=\left\{F,G\right\}$$
3		incat.x	$$⊢\underset{\dot{}}{·}=\left(f\in H,g\in H⟼f\cap g\right)$$
4		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
5	1 4	catbas	$$⊢\left\{X\right\}={\mathrm{Base}}_C$$
6	5	a1i	$$⊢\left(F\subseteq G\wedge G\in V\right)\to \left\{X\right\}={\mathrm{Base}}_C$$
7		snex	$$⊢\left\{⟨X,X,H⟩\right\}\in \mathrm{V}$$
8	1 7	cathomfval	$$⊢\left\{⟨X,X,H⟩\right\}=\mathrm{Hom}\left(C\right)$$
9	8	a1i	$$⊢\left(F\subseteq G\wedge G\in V\right)\to \left\{⟨X,X,H⟩\right\}=\mathrm{Hom}\left(C\right)$$
10		snex	$$⊢\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
11	1 10	catcofval	$$⊢\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}=\mathrm{comp}\left(C\right)$$
12	11	a1i	$$⊢\left(F\subseteq G\wedge G\in V\right)\to \left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}=\mathrm{comp}\left(C\right)$$
13		prex	$$⊢\left\{F,G\right\}\in \mathrm{V}$$
14	2 13	eqeltri	$$⊢H\in \mathrm{V}$$
15	14	ovsn2	$$⊢X\left\{⟨X,X,H⟩\right\}X=H$$
16	15 2	eqtri	$$⊢X\left\{⟨X,X,H⟩\right\}X=\left\{F,G\right\}$$
17	14 14	mpoex	$$⊢\left(f\in H,g\in H⟼f\cap g\right)\in \mathrm{V}$$
18	3 17	eqeltri	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
19	18	ovsn2	$$⊢⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X=\underset{\dot{}}{·}$$
20	19 3	eqtri	$$⊢⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X=\left(f\in H,g\in H⟼f\cap g\right)$$
21	20	a1i	$$⊢\left(F\subseteq G\wedge G\in V\right)\to ⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X=\left(f\in H,g\in H⟼f\cap g\right)$$
22		ineq12	$$⊢\left(f=G\wedge g=G\right)\to f\cap g=G\cap G$$
23		inidm	$$⊢G\cap G=G$$
24	22 23	eqtrdi	$$⊢\left(f=G\wedge g=G\right)\to f\cap g=G$$
25	24	adantl	$$⊢\left(\left(F\subseteq G\wedge G\in V\right)\wedge \left(f=G\wedge g=G\right)\right)\to f\cap g=G$$
26		prid2g	$$⊢G\in V\to G\in \left\{F,G\right\}$$
27	26 2	eleqtrrdi	$$⊢G\in V\to G\in H$$
28	27	adantl	$$⊢\left(F\subseteq G\wedge G\in V\right)\to G\in H$$
29	21 25 28 28 28	ovmpod	$$⊢\left(F\subseteq G\wedge G\in V\right)\to G\left(⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X\right)G=G$$
30		ineq12	$$⊢\left(f=G\wedge g=F\right)\to f\cap g=G\cap F$$
31		sseqin2	$$⊢F\subseteq G\leftrightarrow G\cap F=F$$
32	31	biimpi	$$⊢F\subseteq G\to G\cap F=F$$
33	32	adantr	$$⊢\left(F\subseteq G\wedge G\in V\right)\to G\cap F=F$$
34	30 33	sylan9eqr	$$⊢\left(\left(F\subseteq G\wedge G\in V\right)\wedge \left(f=G\wedge g=F\right)\right)\to f\cap g=F$$
35		ssexg	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\in \mathrm{V}$$
36		prid1g	$$⊢F\in \mathrm{V}\to F\in \left\{F,G\right\}$$
37	35 36	syl	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\in \left\{F,G\right\}$$
38	37 2	eleqtrrdi	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\in H$$
39	21 34 28 38 38	ovmpod	$$⊢\left(F\subseteq G\wedge G\in V\right)\to G\left(⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X\right)F=F$$
40		ineq12	$$⊢\left(f=F\wedge g=G\right)\to f\cap g=F\cap G$$
41		dfss2	$$⊢F\subseteq G\leftrightarrow F\cap G=F$$
42	41	biimpi	$$⊢F\subseteq G\to F\cap G=F$$
43	42	adantr	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\cap G=F$$
44	40 43	sylan9eqr	$$⊢\left(\left(F\subseteq G\wedge G\in V\right)\wedge \left(f=F\wedge g=G\right)\right)\to f\cap g=F$$
45	21 44 38 28 38	ovmpod	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\left(⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X\right)G=F$$
46		ineq12	$$⊢\left(f=F\wedge g=F\right)\to f\cap g=F\cap F$$
47		inidm	$$⊢F\cap F=F$$
48	46 47	eqtrdi	$$⊢\left(f=F\wedge g=F\right)\to f\cap g=F$$
49	48	adantl	$$⊢\left(\left(F\subseteq G\wedge G\in V\right)\wedge \left(f=F\wedge g=F\right)\right)\to f\cap g=F$$
50	21 49 38 38 38	ovmpod	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\left(⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X\right)F=F$$
51	50 37	eqeltrd	$$⊢\left(F\subseteq G\wedge G\in V\right)\to F\left(⟨X,X⟩\left\{⟨⟨X,X⟩,X,\underset{\dot{}}{·}⟩\right\}X\right)F\in \left\{F,G\right\}$$
52	6 9 12 16 29 39 45 51	2arwcat	$$⊢\left(F\subseteq G\wedge G\in V\right)\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(y\in \left\{X\right\}⟼G\right)\right)$$