Theorem inclfusubc

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

	Ref	Expression
Hypotheses	inclfusubc.j	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
	inclfusubc.s	⊢ 𝑆 = ( 𝐶 ↾cat 𝐽 )
	inclfusubc.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	inclfusubc.f	⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
	inclfusubc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) )
Assertion	inclfusubc	⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		inclfusubc.j	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2		inclfusubc.s	⊢ 𝑆 = ( 𝐶 ↾cat 𝐽 )
3		inclfusubc.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		inclfusubc.f	⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
5		inclfusubc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) )
6		fthfunc	⊢ ( 𝑆 Faith 𝐶 ) ⊆ ( 𝑆 Func 𝐶 )
7		eqid	⊢ ( idfunc ‘ 𝑆 ) = ( idfunc ‘ 𝑆 )
8	2 7	rescfth	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Faith 𝐶 ) )
9	1 8	syl	⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Faith 𝐶 ) )
10	6 9	sselid	⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) )
11		df-br	⊢ ( 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 Func 𝐶 ) )
12	4 5	opeq12d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
13	2 7 3	idfusubc	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( idfunc ‘ 𝑆 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
14	1 13	syl	⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
15	12 14	eqtr4d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( idfunc ‘ 𝑆 ) )
16	15	eleq1d	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 Func 𝐶 ) ↔ ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) ) )
17	11 16	bitrid	⊢ ( 𝜑 → ( 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 ↔ ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) ) )
18	10 17	mpbird	⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 )