Metamath Proof Explorer

Theorem idfusubc

Description: The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020)

		Ref	Expression
	Hypotheses	idfusubc.s	$⊢ S = C ↾_{cat} J$
		idfusubc.i	$⊢ I = {id}_{func} (S)$
		idfusubc.b	$⊢ B = {Base}_{S}$
	Assertion	idfusubc	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$

Proof

Step	Hyp	Ref	Expression
1		idfusubc.s	$⊢ S = C ↾_{cat} J$
2		idfusubc.i	$⊢ I = {id}_{func} (S)$
3		idfusubc.b	$⊢ B = {Base}_{S}$
4	1 2 3	idfusubc0	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})⟩$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		subcrcl	$⊢ J \in Subcat (C) \to C \in Cat$
7		id	$⊢ J \in Subcat (C) \to J \in Subcat (C)$
8		eqidd	$⊢ J \in Subcat (C) \to dom dom J = dom dom J$
9	7 8	subcfn	$⊢ J \in Subcat (C) \to J Fn (dom dom J \times dom dom J)$
10	7 9 5	subcss1	$⊢ J \in Subcat (C) \to dom dom J \subseteq {Base}_{C}$
11	1 5 6 9 10	reschom	$⊢ J \in Subcat (C) \to J = Hom (S)$
12	11	eqcomd	$⊢ J \in Subcat (C) \to Hom (S) = J$
13	12	oveqd	$⊢ J \in Subcat (C) \to x Hom (S) y = x J y$
14	13	reseq2d	$⊢ J \in Subcat (C) \to {I ↾}_{(x Hom (S) y)} = {I ↾}_{(x J y)}$
15	14	mpoeq3dv	$⊢ J \in Subcat (C) \to (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)}) = (x \in B, y \in B ⟼ {I ↾}_{(x J y)})$
16	15	opeq2d	$⊢ J \in Subcat (C) \to ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})⟩ = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$
17	4 16	eqtrd	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$