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 ‘ 𝑆 ) 𝑦 ) ) ) ⟩ )