Metamath Proof Explorer

Theorem idfusubc0

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	idfusubc0	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) 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		id	$⊢ J \in Subcat (C) \to J \in Subcat (C)$
5	1 4	subccat	$⊢ J \in Subcat (C) \to S \in Cat$
6		eqid	$⊢ Hom (S) = Hom (S)$
7	2 3 5 6	idfuval	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (z \in (B \times B) ⟼ {I ↾}_{Hom (S) (z)})⟩$
8		fveq2	$⊢ z = ⟨x, y⟩ \to Hom (S) (z) = Hom (S) (⟨x, y⟩)$
9		df-ov	$⊢ x Hom (S) y = Hom (S) (⟨x, y⟩)$
10	8 9	eqtr4di	$⊢ z = ⟨x, y⟩ \to Hom (S) (z) = x Hom (S) y$
11	10	reseq2d	$⊢ z = ⟨x, y⟩ \to {I ↾}_{Hom (S) (z)} = {I ↾}_{(x Hom (S) y)}$
12	11	mpompt	$⊢ (z \in (B \times B) ⟼ {I ↾}_{Hom (S) (z)}) = (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})$
13	12	a1i	$⊢ J \in Subcat (C) \to (z \in (B \times B) ⟼ {I ↾}_{Hom (S) (z)}) = (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})$
14	13	opeq2d	$⊢ J \in Subcat (C) \to ⟨{I ↾}_{B}, (z \in (B \times B) ⟼ {I ↾}_{Hom (S) (z)})⟩ = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})⟩$
15	7 14	eqtrd	$⊢ J \in Subcat (C) \to I = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x Hom (S) y)})⟩$