Metamath Proof Explorer

Theorem fuconuniqvalslem

Description: Lemma for fuconuniqvals . (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 )
fuconuniqvals.d 
|- D = ( E DiagFunc C )
fuconuniqvals.f 
|- F = ( ( 1st ` D ) ` (/) )
fuconuniqvals.g 
|- G = ( ( 1st ` D ) ` 1o )
fuconuniqvals.n 
|- N = ( 1o X. { (/) } )
fuconuniqvalslem.t 
|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
Assertion fuconuniqvalslem 
|- ( ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` L ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = (/) /\ ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` ( K o.func L ) ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = 1o )

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