catsubcat

Description: For any category C , C itself is a (full) subcategory of C , see example 4.3(1.b) in Adamek p. 48. (Contributed by AV, 23-Apr-2020)

		Ref	Expression
	Assertion	catsubcat	$⊢ C \in Cat \to {Hom}_{𝑓} (C) \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		ssidd	$⊢ C \in Cat \to {Base}_{C} \subseteq {Base}_{C}$
2		ssidd	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x {Hom}_{𝑓} (C) y \subseteq x {Hom}_{𝑓} (C) y$
3	2	ralrimivva	$⊢ C \in Cat \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} x {Hom}_{𝑓} (C) y \subseteq x {Hom}_{𝑓} (C) y$
4		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6	4 5	homffn	$⊢ {Hom}_{𝑓} (C) Fn ({Base}_{C} \times {Base}_{C})$
7	6	a1i	$⊢ C \in Cat \to {Hom}_{𝑓} (C) Fn ({Base}_{C} \times {Base}_{C})$
8		fvexd	$⊢ C \in Cat \to {Base}_{C} \in V$
9	7 7 8	isssc	$⊢ C \in Cat \to ({Hom}_{𝑓} (C) \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow ({Base}_{C} \subseteq {Base}_{C} \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} x {Hom}_{𝑓} (C) y \subseteq x {Hom}_{𝑓} (C) y))$
10	1 3 9	mpbir2and	$⊢ C \in Cat \to {Hom}_{𝑓} (C) \subseteq_{cat} {Hom}_{𝑓} (C)$
11		eqid	$⊢ Hom (C) = Hom (C)$
12		eqid	$⊢ Id (C) = Id (C)$
13		simpl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to C \in Cat$
14		simpr	$⊢ (C \in Cat \land x \in {Base}_{C}) \to x \in {Base}_{C}$
15	5 11 12 13 14	catidcl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to Id (C) (x) \in (x Hom (C) x)$
16	4 5 11 14 14	homfval	$⊢ (C \in Cat \land x \in {Base}_{C}) \to x {Hom}_{𝑓} (C) x = x Hom (C) x$
17	15 16	eleqtrrd	$⊢ (C \in Cat \land x \in {Base}_{C}) \to Id (C) (x) \in (x {Hom}_{𝑓} (C) x)$
18		eqid	$⊢ comp (C) = comp (C)$
19	13	adantr	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to C \in Cat$
20	19	adantr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to C \in Cat$
21	14	adantr	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to x \in {Base}_{C}$
22	21	adantr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to x \in {Base}_{C}$
23		simpl	$⊢ (y \in {Base}_{C} \land z \in {Base}_{C}) \to y \in {Base}_{C}$
24	23	adantl	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to y \in {Base}_{C}$
25	24	adantr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to y \in {Base}_{C}$
26		simpr	$⊢ (y \in {Base}_{C} \land z \in {Base}_{C}) \to z \in {Base}_{C}$
27	26	adantl	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to z \in {Base}_{C}$
28	27	adantr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to z \in {Base}_{C}$
29	4 5 11 21 24	homfval	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to x {Hom}_{𝑓} (C) y = x Hom (C) y$
30	29	eleq2d	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to (f \in (x {Hom}_{𝑓} (C) y) \leftrightarrow f \in (x Hom (C) y))$
31	30	biimpcd	$⊢ f \in (x {Hom}_{𝑓} (C) y) \to (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to f \in (x Hom (C) y))$
32	31	adantr	$⊢ (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z)) \to (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to f \in (x Hom (C) y))$
33	32	impcom	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to f \in (x Hom (C) y)$
34	4 5 11 24 27	homfval	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to y {Hom}_{𝑓} (C) z = y Hom (C) z$
35	34	eleq2d	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to (g \in (y {Hom}_{𝑓} (C) z) \leftrightarrow g \in (y Hom (C) z))$
36	35	biimpd	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to (g \in (y {Hom}_{𝑓} (C) z) \to g \in (y Hom (C) z))$
37	36	adantld	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to ((f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z)) \to g \in (y Hom (C) z))$
38	37	imp	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to g \in (y Hom (C) z)$
39	5 11 18 20 22 25 28 33 38	catcocl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)$
40	4 5 11 21 27	homfval	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to x {Hom}_{𝑓} (C) z = x Hom (C) z$
41	40	adantr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to x {Hom}_{𝑓} (C) z = x Hom (C) z$
42	39 41	eleqtrrd	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x {Hom}_{𝑓} (C) y) \land g \in (y {Hom}_{𝑓} (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z)$
43	42	ralrimivva	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to \forall f \in (x {Hom}_{𝑓} (C) y) \forall g \in (y {Hom}_{𝑓} (C) z) g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z)$
44	43	ralrimivva	$⊢ (C \in Cat \land x \in {Base}_{C}) \to \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x {Hom}_{𝑓} (C) y) \forall g \in (y {Hom}_{𝑓} (C) z) g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z)$
45	17 44	jca	$⊢ (C \in Cat \land x \in {Base}_{C}) \to (Id (C) (x) \in (x {Hom}_{𝑓} (C) x) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x {Hom}_{𝑓} (C) y) \forall g \in (y {Hom}_{𝑓} (C) z) g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z))$
46	45	ralrimiva	$⊢ C \in Cat \to \forall x \in {Base}_{C} (Id (C) (x) \in (x {Hom}_{𝑓} (C) x) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x {Hom}_{𝑓} (C) y) \forall g \in (y {Hom}_{𝑓} (C) z) g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z))$
47		id	$⊢ C \in Cat \to C \in Cat$
48	4 12 18 47 7	issubc2	$⊢ C \in Cat \to ({Hom}_{𝑓} (C) \in Subcat (C) \leftrightarrow ({Hom}_{𝑓} (C) \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in {Base}_{C} (Id (C) (x) \in (x {Hom}_{𝑓} (C) x) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x {Hom}_{𝑓} (C) y) \forall g \in (y {Hom}_{𝑓} (C) z) g (⟨x, y⟩ comp (C) z) f \in (x {Hom}_{𝑓} (C) z))))$
49	10 46 48	mpbir2and	$⊢ C \in Cat \to {Hom}_{𝑓} (C) \in Subcat (C)$

Metamath Proof Explorer

Theorem catsubcat

Proof