Metamath Proof Explorer

Theorem par2str

Description: The object set, hom operation, and composition of the concrete two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypothesis par2str.c 
|- C = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
Assertion par2str 
|- ( 2o = ( Base ` C ) /\ ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` C ) /\ ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) = ( comp ` C ) )

Proof

Step Hyp Ref Expression
1 par2str.c 
 |-  C = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
2 2oex 
 |-  2o e. _V
3 1 2 catbas 
 |-  2o = ( Base ` C )
4 2 2 mpoex 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) e. _V
5 1 4 cathomfval 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` C )
6 2 2 xpex 
 |-  ( 2o X. 2o ) e. _V
7 6 2 mpoex 
 |-  ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) e. _V
8 1 7 catcofval 
 |-  ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) = ( comp ` C )
9 3 5 8 3pm3.2i 
 |-  ( 2o = ( Base ` C ) /\ ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` C ) /\ ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) = ( comp ` C ) )