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 ⊢ S = C ↾ cat J
idfusubc.i ⊢ I = id func ⁡ S
idfusubc.b ⊢ B = Base S
Assertion idfusubc ⊢ J ∈ Subcat ⁡ C → I = I ↾ B x ∈ B , y ∈ B ⟼ I ↾ x J y

Proof

Step Hyp Ref Expression
1 idfusubc.s ⊢ S = C ↾ cat J
2 idfusubc.i ⊢ I = id func ⁡ S
3 idfusubc.b ⊢ B = Base S
4 1 2 3 idfusubc0 ⊢ J ∈ Subcat ⁡ C → I = I ↾ B x ∈ B , y ∈ B ⟼ I ↾ x Hom ⁡ S y
5 eqid ⊢ Base C = Base C
6 subcrcl ⊢ J ∈ Subcat ⁡ C → C ∈ Cat
7 id ⊢ J ∈ Subcat ⁡ C → J ∈ Subcat ⁡ C
8 eqidd ⊢ J ∈ Subcat ⁡ C → dom ⁡ dom ⁡ J = dom ⁡ dom ⁡ J
9 7 8 subcfn ⊢ J ∈ Subcat ⁡ C → J Fn dom ⁡ dom ⁡ J × dom ⁡ dom ⁡ J
10 7 9 5 subcss1 ⊢ J ∈ Subcat ⁡ C → dom ⁡ dom ⁡ J ⊆ Base C
11 1 5 6 9 10 reschom ⊢ J ∈ Subcat ⁡ C → J = Hom ⁡ S
12 11 eqcomd ⊢ J ∈ Subcat ⁡ C → Hom ⁡ S = J
13 12 oveqd ⊢ J ∈ Subcat ⁡ C → x Hom ⁡ S y = x J y
14 13 reseq2d ⊢ J ∈ Subcat ⁡ C → I ↾ x Hom ⁡ S y = I ↾ x J y
15 14 mpoeq3dv ⊢ J ∈ Subcat ⁡ C → x ∈ B , y ∈ B ⟼ I ↾ x Hom ⁡ S y = x ∈ B , y ∈ B ⟼ I ↾ x J y
16 15 opeq2d ⊢ J ∈ Subcat ⁡ C → I ↾ B x ∈ B , y ∈ B ⟼ I ↾ x Hom ⁡ S y = I ↾ B x ∈ B , y ∈ B ⟼ I ↾ x J y
17 4 16 eqtrd ⊢ J ∈ Subcat ⁡ C → I = I ↾ B x ∈ B , y ∈ B ⟼ I ↾ x J y