Theorem fuconuniqlem

Description: Lemma for fuconuniq . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

	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 )
	fuconuniqlem.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
	fuconuniqlem.d	|- D = ( E DiagFunc C )
	fuconuniqlem.f	|- F = ( ( 1st ` D ) ` (/) )
	fuconuniqlem.g	|- G = ( ( 1st ` D ) ` 1o )
	fuconuniqlem.n	|- N = ( 1o X. { (/) } )
Assertion	fuconuniqlem	|- ( ( 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		fuconuniqlem.t	|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
12		fuconuniqlem.d	|- D = ( E DiagFunc C )
13		fuconuniqlem.f	|- F = ( ( 1st ` D ) ` (/) )
14		fuconuniqlem.g	|- G = ( ( 1st ` D ) ` 1o )
15		fuconuniqlem.n	|- N = ( 1o X. { (/) } )
16		setc1oterm	|- ( SetCat ` 1o ) e. TermCat
17	1 16	eqeltri	|- C e. TermCat
18	17	a1i	|- ( T. -> C e. TermCat )
19	18	termccatd	|- ( T. -> C e. Cat )
20	2	par2catid	|- ( E e. Cat /\ ( Id ` E ) = ( y e. 2o |-> 2o ) )
21	20	simpli	|- E e. Cat
22	21	a1i	|- ( T. -> E e. Cat )
23	2 5 6	parswapfunc	|- <. ( _I |` 2o ) , M >. e. ( E Func E )
24	7 23	eqeltri	|- S e. ( E Func E )
25	24	a1i	|- ( T. -> S e. ( E Func E ) )
26		mptresid	|- ( _I |` 2o ) = ( x e. 2o |-> x )
27		2oex	|- 2o e. _V
28	27	mptex	|- ( x e. 2o |-> x ) e. _V
29	26 28	eqeltri	|- ( _I |` 2o ) e. _V
30	27 27	mpoex	|- ( 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 ) ) ) e. _V
31	6 30	eqeltri	|- M e. _V
32	29 31	op1std	|- ( S = <. ( _I |` 2o ) , M >. -> ( 1st ` S ) = ( _I |` 2o ) )
33	7 32	mp1i	|- ( T. -> ( 1st ` S ) = ( _I |` 2o ) )
34	18 3 8 9 10 25 33	termcpostfix	|- ( T. -> ( K e. ( Q Func Q ) /\ ( 1st ` K ) = ( _I |` ( C Func E ) ) ) )
35	34	simpld	|- ( T. -> K e. ( Q Func Q ) )
36	34	simprd	|- ( T. -> ( 1st ` K ) = ( _I |` ( C Func E ) ) )
37	3 11 4 19 19 22 35 36	fucoaltfunc	|- ( T. -> ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) )
38	1 2 12 13 14 15	par2diag	|- ( ( F e. ( C Func E ) /\ G e. ( C Func E ) ) /\ ( N e. ( F ( C Nat E ) G ) /\ ( N ` (/) ) = (/) ) /\ ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o ) )
39	38	simp1i	|- ( F e. ( C Func E ) /\ G e. ( C Func E ) )
40	39	simpli	|- F e. ( C Func E )
41	40	a1i	|- ( T. -> F e. ( C Func E ) )
42	39	simpri	|- G e. ( C Func E )
43	42	a1i	|- ( T. -> G e. ( C Func E ) )
44	38	simp2i	|- ( N e. ( F ( C Nat E ) G ) /\ ( N ` (/) ) = (/) )
45	44	simpli	|- N e. ( F ( C Nat E ) G )
46	45	a1i	|- ( T. -> N e. ( F ( C Nat E ) G ) )
47		0lt1o	|- (/) e. 1o
48	1	setc1obas	|- 1o = ( Base ` C )
49	47 48	eleqtri	|- (/) e. ( Base ` C )
50	49	a1i	|- ( T. -> (/) e. ( Base ` C ) )
51	3 8 9 25 19 10 41 43 46 50	postcof2	|- ( T. -> ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) = ( ( ( ( 1st ` F ) ` (/) ) ( 2nd ` S ) ( ( 1st ` G ) ` (/) ) ) ` ( N ` (/) ) ) )
52	51	mptru	|- ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) = ( ( ( ( 1st ` F ) ` (/) ) ( 2nd ` S ) ( ( 1st ` G ) ` (/) ) ) ` ( N ` (/) ) )
53	38	simp3i	|- ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o )
54	53	simpli	|- ( ( 1st ` F ) ` (/) ) = (/)
55	53	simpri	|- ( ( 1st ` G ) ` (/) ) = 1o
56	29 31	op2ndd	|- ( S = <. ( _I |` 2o ) , M >. -> ( 2nd ` S ) = M )
57	7 56	ax-mp	|- ( 2nd ` S ) = M
58	54 55 57	oveq123i	|- ( ( ( 1st ` F ) ` (/) ) ( 2nd ` S ) ( ( 1st ` G ) ` (/) ) ) = ( (/) M 1o )
59	44	simpri	|- ( N ` (/) ) = (/)
60	58 59	fveq12i	|- ( ( ( ( 1st ` F ) ` (/) ) ( 2nd ` S ) ( ( 1st ` G ) ` (/) ) ) ` ( N ` (/) ) ) = ( ( (/) M 1o ) ` (/) )
61	52 60	eqtri	|- ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) = ( ( (/) M 1o ) ` (/) )
62		0ex	|- (/) e. _V
63	62	prid1	|- (/) e. { (/) , 1o }
64		df2o3	|- 2o = { (/) , 1o }
65	63 64	eleqtrri	|- (/) e. 2o
66	65	a1i	|- ( T. -> (/) e. 2o )
67		1oelpr	|- 1o e. { (/) , 1o }
68	67 64	eleqtrri	|- 1o e. 2o
69	68	a1i	|- ( T. -> 1o e. 2o )
70		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 , (/) ) ) )
71	70	par2hom	|- ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = { 2o } /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = { 2o } /\ ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = (/) ) )
72	71	simp3i	|- ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = (/) )
73	72	simpli	|- ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o
74	65 73	eleqtrri	|- (/) e. ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o )
75	74	a1i	|- ( T. -> (/) e. ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) )
76	6 66 69 75	fvmpomptd	|- ( T. -> ( ( (/) M 1o ) ` (/) ) = ( A ` (/) ) )
77	76	mptru	|- ( ( (/) M 1o ) ` (/) ) = ( A ` (/) )
78	5	parswapprop	|- ( ( A ` 2o ) = 2o /\ A. t e. 2o ( A ` t ) e. 2o /\ ( A ` (/) ) = 1o )
79	78	simp3i	|- ( A ` (/) ) = 1o
80	61 77 79	3eqtri	|- ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) = 1o
81		1n0	|- 1o =/= (/)
82	80 81	eqnetri	|- ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) =/= (/)
83	82 59	neeqtrri	|- ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) =/= ( N ` (/) )
84		fveq1	|- ( ( ( F ( 2nd ` K ) G ) ` N ) = N -> ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) = ( N ` (/) ) )
85	84	necon3i	|- ( ( ( ( F ( 2nd ` K ) G ) ` N ) ` (/) ) =/= ( N ` (/) ) -> ( ( F ( 2nd ` K ) G ) ` N ) =/= N )
86	83 85	mp1i	|- ( T. -> ( ( F ( 2nd ` K ) G ) ` N ) =/= N )
87	3 4 19 22 35 41 43 46 86	fucoaltne	|- ( T. -> ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )
88	37 87	jca	|- ( T. -> ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) /\ ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) ) )
89	88	mptru	|- ( ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) /\ ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )