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

Proof

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

Metamath Proof Explorer

Theorem incat

Proof