Metamath Proof Explorer

Theorem parswapfunc

Description: The explicit exchange of the two parallel nonidentity arrows is an endofunctor with identity object function. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses parswapfunc.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 ) ) ) >. }
parswapfunc.a 
|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
parswapfunc.l 
|- L = ( u e. 2o , v e. 2o |-> ( a e. ( u ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) v ) |-> ( A ` a ) ) )
Assertion parswapfunc 
|- <. ( _I |` 2o ) , L >. e. ( C Func C )

Proof

Step Hyp Ref Expression
1 parswapfunc.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 parswapfunc.a 
 |-  A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
3 parswapfunc.l 
 |-  L = ( u e. 2o , v e. 2o |-> ( a e. ( u ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) v ) |-> ( A ` a ) ) )
4 1 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 ) )
5 4 simp1i 
 |-  2o = ( Base ` C )
6 4 simp2i 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` C )
7 1 par2catid 
 |-  ( C e. Cat /\ ( Id ` C ) = ( t e. 2o |-> 2o ) )
8 7 simpli 
 |-  C e. Cat
9 eqid 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) )
10 2 parswapprop 
 |-  ( ( A ` 2o ) = 2o /\ A. t e. 2o ( A ` t ) e. 2o /\ ( A ` (/) ) = 1o )
11 10 simp1i 
 |-  ( A ` 2o ) = 2o
12 10 simp2i 
 |-  A. t e. 2o ( A ` t ) e. 2o
13 5 6 8 9 3 11 12 parmapfunc 
 |-  ( _I |` 2o ) ( C Func C ) L
14 df-br 
 |-  ( ( _I |` 2o ) ( C Func C ) L <-> <. ( _I |` 2o ) , L >. e. ( C Func C ) )
15 13 14 mpbi 
 |-  <. ( _I |` 2o ) , L >. e. ( C Func C )