# 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 𝑆 = ( 𝐶cat 𝐽 )
idfusubc.i 𝐼 = ( idfunc𝑆 )
idfusubc.b 𝐵 = ( Base ‘ 𝑆 )
Assertion idfusubc ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )

### Proof

Step Hyp Ref Expression
1 idfusubc.s 𝑆 = ( 𝐶cat 𝐽 )
2 idfusubc.i 𝐼 = ( idfunc𝑆 )
3 idfusubc.b 𝐵 = ( Base ‘ 𝑆 )
4 1 2 3 idfusubc0 ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) ⟩ )
5 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 subcrcl ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
7 id ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
8 eqidd ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → dom dom 𝐽 = dom dom 𝐽 )
9 7 8 subcfn ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
10 7 9 5 subcss1 ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → dom dom 𝐽 ⊆ ( Base ‘ 𝐶 ) )
11 1 5 6 9 10 reschom ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐽 = ( Hom ‘ 𝑆 ) )
12 11 eqcomd ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( Hom ‘ 𝑆 ) = 𝐽 )
13 12 oveqd ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
14 13 reseq2d ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) = ( I ↾ ( 𝑥 𝐽 𝑦 ) ) )
15 14 mpoeq3dv ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) )
16 15 opeq2d ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
17 4 16 eqtrd ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )