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 ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )