# Metamath Proof Explorer

## 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 sseldi ( 𝜑 → ( 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 syl5bb ( 𝜑 → ( 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 ↔ ( idfunc𝑆 ) ∈ ( 𝑆 Func 𝐶 ) ) )
18 10 17 mpbird ( 𝜑𝐹 ( 𝑆 Func 𝐶 ) 𝐺 )