Theorem fuconuniq

Description: The arrow map A fixes the identity arrow 2o and exchanges the two nonidentity parallel arrows (/) and 1o . It gives a concrete alternative to functor composition with the same object function and a different morphism function. All hypotheses name explicit constructed sets; no category or functor existence is assumed. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fuconuniq2.c	|- C = ( SetCat ` 1o )
	fuconuniq2.e	|- E = { <. ( 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 ) ) ) >. }
	fuconuniq2.q	|- Q = ( C FuncCat E )
	fuconuniq2.l	|- L = ( <. C , C >. o.F E )
	fuconuniq.a	|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
	fuconuniq.m	|- M = ( 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 ) ) )
	fuconuniq.s	|- S = <. ( _I |` 2o ) , M >.
	fuconuniq.r	|- R = ( E FuncCat E )
	fuconuniq.o	|- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) )
	fuconuniq.k	|- K = ( ( 1st ` .o. ) ` S )
	fuconuniq.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
Assertion	fuconuniq	|- ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) /\ ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	|- C = ( SetCat ` 1o )
2		fuconuniq2.e	|- E = { <. ( 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 ) ) ) >. }
3		fuconuniq2.q	|- Q = ( C FuncCat E )
4		fuconuniq2.l	|- L = ( <. C , C >. o.F E )
5		fuconuniq.a	|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
6		fuconuniq.m	|- M = ( 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 ) ) )
7		fuconuniq.s	|- S = <. ( _I |` 2o ) , M >.
8		fuconuniq.r	|- R = ( E FuncCat E )
9		fuconuniq.o	|- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) )
10		fuconuniq.k	|- K = ( ( 1st ` .o. ) ` S )
11		fuconuniq.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
12		eqid	|- ( E DiagFunc C ) = ( E DiagFunc C )
13		eqid	|- ( ( 1st ` ( E DiagFunc C ) ) ` (/) ) = ( ( 1st ` ( E DiagFunc C ) ) ` (/) )
14		eqid	|- ( ( 1st ` ( E DiagFunc C ) ) ` 1o ) = ( ( 1st ` ( E DiagFunc C ) ) ` 1o )
15		eqid	|- ( 1o X. { (/) } ) = ( 1o X. { (/) } )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	fuconuniqlem	|- ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) /\ ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )