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

### Proof

Step Hyp Ref Expression
1 idfusubc.s 𝑆 = ( 𝐶cat 𝐽 )
2 idfusubc.i 𝐼 = ( idfunc𝑆 )
3 idfusubc.b 𝐵 = ( Base ‘ 𝑆 )
4 id ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
5 1 4 subccat ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝑆 ∈ Cat )
6 eqid ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
7 2 3 5 6 idfuval ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) ) ) ⟩ )
8 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝑆 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
9 df-ov ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) = ( ( Hom ‘ 𝑆 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
10 8 9 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) = ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) )
11 10 reseq2d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( I ↾ ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) )
12 11 mpompt ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) )
13 12 a1i ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) )
14 13 opeq2d ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝑆 ) ‘ 𝑧 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) ⟩ )
15 7 14 eqtrd ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ) ) ⟩ )