Metamath Proof Explorer

Theorem cnelsubc

Description: Remark 4.2(2) of Adamek p. 48. There exists acategory satisfying all conditions for a subcategory but the compatibility of identity morphisms. Therefore such condition in df-subc is necessary. A stronger statement than nelsubc3 . (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Assertion cnelsubc 
|- E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Homf ` ( SetCat ` 1o ) ) e. _V
2 1oex 
 |-  1o e. _V
3 eqid 
 |-  { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } = { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. }
4 eqid 
 |-  ( f e. 2o , g e. 2o |-> ( f i^i g ) ) = ( f e. 2o , g e. 2o |-> ( f i^i g ) )
5 eqid 
 |-  ( SetCat ` 1o ) = ( SetCat ` 1o )
6 eqid 
 |-  ( Homf ` ( SetCat ` 1o ) ) = ( Homf ` ( SetCat ` 1o ) )
7 eqid 
 |-  1o = 1o
8 eqid 
 |-  ( Homf ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } ) = ( Homf ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } )
9 eqid 
 |-  ( Id ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } ) = ( Id ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } )
10 eqid 
 |-  ( { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } |`cat ( Homf ` ( SetCat ` 1o ) ) ) = ( { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } |`cat ( Homf ` ( SetCat ` 1o ) ) )
11 3 4 5 6 7 8 9 10 setc1onsubc 
 |-  ( { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } e. Cat /\ ( Homf ` ( SetCat ` 1o ) ) Fn ( 1o X. 1o ) /\ ( ( Homf ` ( SetCat ` 1o ) ) C_cat ( Homf ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } ) /\ -. A. x e. 1o ( ( Id ` { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } ) ` x ) e. ( x ( Homf ` ( SetCat ` 1o ) ) x ) /\ ( { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , ( f e. 2o , g e. 2o |-> ( f i^i g ) ) >. } >. } |`cat ( Homf ` ( SetCat ` 1o ) ) ) e. Cat ) )
12 1 2 11 cnelsubclem 
 |-  E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) )