Metamath Proof Explorer

Theorem parcatid2

Description: Variant of parcatid . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses parcatid.b 
|- B e. _V
parcatid.j 
|- J e. _V
parcatid.p 
|- S C_ ~P J
parcatid.k 
|- K = ( S u. { J } )
parcatid.h 
|- H = ( m e. B , n e. B |-> if ( m = n , { J } , if ( ( m = X /\ n = Y ) , S , (/) ) ) )
parcatid.m 
|- M = ( r e. K , s e. K |-> ( r i^i s ) )
parcatid.o 
|- .x. = ( p e. ( B X. B ) , q e. B |-> M )
parcatid.c 
|- C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
parcatid2.s 
|- S e. _V
parcatid2.n 
|- X =/= Y
Assertion parcatid2 
|- ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> J ) )

Proof

Step Hyp Ref Expression
1 parcatid.b 
 |-  B e. _V
2 parcatid.j 
 |-  J e. _V
3 parcatid.p 
 |-  S C_ ~P J
4 parcatid.k 
 |-  K = ( S u. { J } )
5 parcatid.h 
 |-  H = ( m e. B , n e. B |-> if ( m = n , { J } , if ( ( m = X /\ n = Y ) , S , (/) ) ) )
6 parcatid.m 
 |-  M = ( r e. K , s e. K |-> ( r i^i s ) )
7 parcatid.o 
 |-  .x. = ( p e. ( B X. B ) , q e. B |-> M )
8 parcatid.c 
 |-  C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
9 parcatid2.s 
 |-  S e. _V
10 parcatid2.n 
 |-  X =/= Y
11 8 1 catbas 
 |-  B = ( Base ` C )
12 11 a1i 
 |-  ( T. -> B = ( Base ` C ) )
13 1 1 mpoex 
 |-  ( m e. B , n e. B |-> if ( m = n , { J } , if ( ( m = X /\ n = Y ) , S , (/) ) ) ) e. _V
14 5 13 eqeltri 
 |-  H e. _V
15 8 14 cathomfval 
 |-  H = ( Hom ` C )
16 15 a1i 
 |-  ( T. -> H = ( Hom ` C ) )
17 1 1 xpex 
 |-  ( B X. B ) e. _V
18 17 1 mpoex 
 |-  ( p e. ( B X. B ) , q e. B |-> M ) e. _V
19 7 18 eqeltri 
 |-  .x. e. _V
20 8 19 catcofval 
 |-  .x. = ( comp ` C )
21 20 a1i 
 |-  ( T. -> .x. = ( comp ` C ) )
22 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
23 8 22 eqeltri 
 |-  C e. _V
24 23 a1i 
 |-  ( T. -> C e. _V )
25 biid 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
26 simpr 
 |-  ( ( T. /\ y e. B ) -> y e. B )
27 5 2 26 parhomid 
 |-  ( ( T. /\ y e. B ) -> J e. ( y H y ) )
28 snex 
 |-  { J } e. _V
29 9 28 unex 
 |-  ( S u. { J } ) e. _V
30 4 29 eqeltri 
 |-  K e. _V
31 30 30 mpoex 
 |-  ( r e. K , s e. K |-> ( r i^i s ) ) e. _V
32 6 31 eqeltri 
 |-  M e. _V
33 simpr 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
34 33 simp1d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( x e. B /\ y e. B ) )
35 34 simpld 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> x e. B )
36 34 simprd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> y e. B )
37 33 simp3d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) )
38 37 simp1d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> f e. ( x H y ) )
39 5 4 38 parhomcl 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> f e. K )
40 2 snid 
 |-  J e. { J }
41 elun2 
 |-  ( J e. { J } -> J e. ( S u. { J } ) )
42 40 41 ax-mp 
 |-  J e. ( S u. { J } )
43 42 4 eleqtrri 
 |-  J e. K
44 43 a1i 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> J e. K )
45 6 7 32 35 36 36 39 44 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( J ( <. x , y >. .x. y ) f ) = ( J i^i f ) )
46 5 3 38 parhomss 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> f C_ J )
47 sseqin2 
 |-  ( f C_ J <-> ( J i^i f ) = f )
48 46 47 sylib 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( J i^i f ) = f )
49 45 48 eqtrd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( J ( <. x , y >. .x. y ) f ) = f )
50 33 simp2d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( z e. B /\ w e. B ) )
51 50 simpld 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> z e. B )
52 37 simp2d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> g e. ( y H z ) )
53 5 4 52 parhomcl 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> g e. K )
54 6 7 32 36 36 51 44 53 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. y , y >. .x. z ) J ) = ( g i^i J ) )
55 5 3 52 parhomss 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> g C_ J )
56 dfss2 
 |-  ( g C_ J <-> ( g i^i J ) = g )
57 55 56 sylib 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g i^i J ) = g )
58 54 57 eqtrd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. y , y >. .x. z ) J ) = g )
59 6 7 32 35 36 51 39 53 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) = ( g i^i f ) )
60 5 38 52 3 parhomco 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g i^i f ) e. ( x H z ) )
61 59 60 eqeltrd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
62 inass 
 |-  ( ( k i^i g ) i^i f ) = ( k i^i ( g i^i f ) )
63 50 simprd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> w e. B )
64 37 simp3d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> k e. ( z H w ) )
65 5 4 64 parhomcl 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> k e. K )
66 6 7 32 36 51 63 53 65 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. y , z >. .x. w ) g ) = ( k i^i g ) )
67 66 oveq1d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( k i^i g ) ( <. x , y >. .x. w ) f ) )
68 5 52 64 3 parhomco 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k i^i g ) e. ( y H w ) )
69 5 4 68 parhomcl 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k i^i g ) e. K )
70 6 7 32 35 36 63 39 69 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k i^i g ) ( <. x , y >. .x. w ) f ) = ( ( k i^i g ) i^i f ) )
71 67 70 eqtrd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( k i^i g ) i^i f ) )
72 59 oveq2d 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( k ( <. x , z >. .x. w ) ( g i^i f ) ) )
73 5 4 60 parhomcl 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g i^i f ) e. K )
74 6 7 32 35 51 63 73 65 parcoval 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. x , z >. .x. w ) ( g i^i f ) ) = ( k i^i ( g i^i f ) ) )
75 72 74 eqtrd 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( k i^i ( g i^i f ) ) )
76 62 71 75 3eqtr4a 
 |-  ( ( T. /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
77 12 16 21 24 25 27 49 58 61 76 iscatd2 
 |-  ( T. -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> J ) ) )
78 77 mptru 
 |-  ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> J ) )