inclfusubc

Description: The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020)

Step	Hyp	Ref	Expression
1		inclfusubc.j	$⊢ φ \to J \in Subcat (C)$
2		inclfusubc.s	$⊢ S = C ↾_{cat} J$
3		inclfusubc.b	$⊢ B = {Base}_{S}$
4		inclfusubc.f	$⊢ φ \to F = {I ↾}_{B}$
5		inclfusubc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x J y)})$
6		fthfunc	$⊢ S Faith C \subseteq S Func C$
7		eqid	$⊢ {id}_{func} (S) = {id}_{func} (S)$
8	2 7	rescfth	$⊢ J \in Subcat (C) \to {id}_{func} (S) \in (S Faith C)$
9	1 8	syl	$⊢ φ \to {id}_{func} (S) \in (S Faith C)$
10	6 9	sselid	$⊢ φ \to {id}_{func} (S) \in (S Func C)$
11		df-br	$⊢ F (S Func C) G \leftrightarrow ⟨F, G⟩ \in (S Func C)$
12	4 5	opeq12d	$⊢ φ \to ⟨F, G⟩ = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$
13	2 7 3	idfusubc	$⊢ J \in Subcat (C) \to {id}_{func} (S) = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$
14	1 13	syl	$⊢ φ \to {id}_{func} (S) = ⟨{I ↾}_{B}, (x \in B, y \in B ⟼ {I ↾}_{(x J y)})⟩$
15	12 14	eqtr4d	$⊢ φ \to ⟨F, G⟩ = {id}_{func} (S)$
16	15	eleq1d	$⊢ φ \to (⟨F, G⟩ \in (S Func C) \leftrightarrow {id}_{func} (S) \in (S Func C))$
17	11 16	bitrid	$⊢ φ \to (F (S Func C) G \leftrightarrow {id}_{func} (S) \in (S Func C))$
18	10 17	mpbird	$⊢ φ \to F (S Func C) G$

Metamath Proof Explorer