Theorem fuconuniq2

Description: The concrete parallel-arrow category supplies a morphism function different from canonical functor composition, with its object function fixed exactly. See par2cat and par2hom for the category and its four hom-sets. (Contributed by Zhi Wang, 14-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 )
	fuconuniq2.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
Assertion	fuconuniq2	|- E. z ( ( 1st ` L ) ( T Func Q ) z /\ z =/= ( 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		fuconuniq2.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
6		fvex	|- ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) e. _V
7		breq2	|- ( z = ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) -> ( ( 1st ` L ) ( T Func Q ) z <-> ( 1st ` L ) ( T Func Q ) ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) ) )
8		neeq1	|- ( z = ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) -> ( z =/= ( 2nd ` L ) <-> ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) =/= ( 2nd ` L ) ) )
9	7 8	anbi12d	|- ( z = ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) -> ( ( ( 1st ` L ) ( T Func Q ) z /\ z =/= ( 2nd ` L ) ) <-> ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) /\ ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) =/= ( 2nd ` L ) ) ) )
10		eqid	|- ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
11		eqid	|- ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) = ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) )
12		eqid	|- <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. = <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >.
13		eqid	|- ( E FuncCat E ) = ( E FuncCat E )
14		eqid	|- ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) = ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) )
15		eqid	|- ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) = ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. )
16	1 2 3 4 10 11 12 13 14 15 5	fuconuniq	|- ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) /\ ( 2nd ` ( ( ( 1st ` ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) ) ` <. ( _I |` 2o ) , ( 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 ) |-> ( ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) ) ` a ) ) ) >. ) o.func L ) ) =/= ( 2nd ` L ) )
17	6 9 16	ceqsexv2d	|- E. z ( ( 1st ` L ) ( T Func Q ) z /\ z =/= ( 2nd ` L ) )