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=\mathrm{SetCat}\left(1_{𝑜}\right)$$
	fuconuniq2.e	$$⊢E=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
	fuconuniq2.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fuconuniq2.l	No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
	fuconuniq2.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
Assertion	fuconuniq2	$$⊢\exists z\left(1^{st}\left(L\right)\left(T\mathrm{Func}Q\right)z\wedge z\ne 2^{nd}\left(L\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	$$⊢C=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		fuconuniq2.e	$$⊢E=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
3		fuconuniq2.q	$$⊢Q=C\mathrm{FuncCat}E$$
4		fuconuniq2.l	Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
5		fuconuniq2.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
6		fvex	Could not format ( 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 : No typesetting found for |- ( 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 with typecode |-
7		breq2	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
8		neeq1	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
9	7 8	anbi12d	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
10		eqid	$$⊢\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)=\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)$$
11		eqid	$$⊢\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)\left(a\right)\right)\right)=\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)\left(a\right)\right)\right)$$
12		eqid	$$⊢⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)\left(a\right)\right)\right)⟩=⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)\left(a\right)\right)\right)⟩$$
13		eqid	$$⊢E\mathrm{FuncCat}E=E\mathrm{FuncCat}E$$
14		eqid	Could not format ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) = ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) : No typesetting found for |- ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) = ( <. ( E FuncCat E ) , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
15		eqid	Could not format ( ( 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 ) ) ) >. ) : No typesetting found for |- ( ( 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 ) ) ) >. ) with typecode |-
16	1 2 3 4 10 11 12 13 14 15 5	fuconuniq	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
17	6 9 16	ceqsexv2d	$$⊢\exists z\left(1^{st}\left(L\right)\left(T\mathrm{Func}Q\right)z\wedge z\ne 2^{nd}\left(L\right)\right)$$