Metamath Proof Explorer

Theorem subcidcl

Description: The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j ${⊢}{\phi }\to {J}\in \mathrm{Subcat}\left({C}\right)$
subcidcl.2 ${⊢}{\phi }\to {J}Fn\left({S}×{S}\right)$
subcidcl.x ${⊢}{\phi }\to {X}\in {S}$
subcidcl.1
Assertion subcidcl

Proof

Step Hyp Ref Expression
1 subcidcl.j ${⊢}{\phi }\to {J}\in \mathrm{Subcat}\left({C}\right)$
2 subcidcl.2 ${⊢}{\phi }\to {J}Fn\left({S}×{S}\right)$
3 subcidcl.x ${⊢}{\phi }\to {X}\in {S}$
4 subcidcl.1
5 fveq2
6 id ${⊢}{x}={X}\to {x}={X}$
7 6 6 oveq12d ${⊢}{x}={X}\to {x}{J}{x}={X}{J}{X}$
8 5 7 eleq12d
9 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
10 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
11 subcrcl ${⊢}{J}\in \mathrm{Subcat}\left({C}\right)\to {C}\in \mathrm{Cat}$
12 1 11 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
13 9 4 10 12 2 issubc2
14 1 13 mpbid
15 simpl
16 15 ralimi
17 14 16 simpl2im
18 8 17 3 rspcdva