fuconuniqvalslem

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

	Ref	Expression
Hypotheses	fuconuniq2.c	⊢ 𝐶 = ( SetCat ‘ 1_o )
	fuconuniq2.e	⊢ 𝐸 = { ⟨ ( Base ‘ ndx ) , 2_o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2_o × 2_o ) , 𝑞 ∈ 2_o ↦ ( 𝑟 ∈ 3_o , 𝑠 ∈ 3_o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
	fuconuniq2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fuconuniq2.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
	fuconuniq.a	⊢ 𝐴 = ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) )
	fuconuniq.m	⊢ 𝑀 = ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
	fuconuniq.s	⊢ 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩
	fuconuniq.r	⊢ 𝑅 = ( 𝐸 FuncCat 𝐸 )
	fuconuniq.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) )
	fuconuniq.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝑆 )
	fuconuniqvals.d	⊢ 𝐷 = ( 𝐸 Δ_func 𝐶 )
	fuconuniqvals.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐷 ) ‘ ∅ )
	fuconuniqvals.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐷 ) ‘ 1_o )
	fuconuniqvals.n	⊢ 𝑁 = ( 1_o × { ∅ } )
	fuconuniqvalslem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
Assertion	fuconuniqvalslem	⊢ ( ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ∅ ∧ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = 1_o )

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	⊢ 𝐶 = ( SetCat ‘ 1_o )
2		fuconuniq2.e	⊢ 𝐸 = { ⟨ ( Base ‘ ndx ) , 2_o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2_o × 2_o ) , 𝑞 ∈ 2_o ↦ ( 𝑟 ∈ 3_o , 𝑠 ∈ 3_o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
3		fuconuniq2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
4		fuconuniq2.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
5		fuconuniq.a	⊢ 𝐴 = ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) )
6		fuconuniq.m	⊢ 𝑀 = ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
7		fuconuniq.s	⊢ 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩
8		fuconuniq.r	⊢ 𝑅 = ( 𝐸 FuncCat 𝐸 )
9		fuconuniq.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) )
10		fuconuniq.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝑆 )
11		fuconuniqvals.d	⊢ 𝐷 = ( 𝐸 Δ_func 𝐶 )
12		fuconuniqvals.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐷 ) ‘ ∅ )
13		fuconuniqvals.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐷 ) ‘ 1_o )
14		fuconuniqvals.n	⊢ 𝑁 = ( 1_o × { ∅ } )
15		fuconuniqvalslem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
16	4	eqcomi	⊢ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) = 𝐿
17	16	fveq2i	⊢ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) ) = ( 2^nd ‘ 𝐿 )
18	17	a1i	⊢ ( ⊤ → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) ) = ( 2^nd ‘ 𝐿 ) )
19		eqid	⊢ ( 𝐶 FuncCat 𝐶 ) = ( 𝐶 FuncCat 𝐶 )
20		eqid	⊢ ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
21		eqid	⊢ ( id_func ‘ 𝐶 ) = ( id_func ‘ 𝐶 )
22		setc1oterm	⊢ ( SetCat ‘ 1_o ) ∈ TermCat
23	1 22	eqeltri	⊢ 𝐶 ∈ TermCat
24	23	a1i	⊢ ( ⊤ → 𝐶 ∈ TermCat )
25	24	termccatd	⊢ ( ⊤ → 𝐶 ∈ Cat )
26	1 2 11 12 13 14	par2diag	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) ∧ ( 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝑁 ‘ ∅ ) = ∅ ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) )
27	26	simp2i	⊢ ( 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝑁 ‘ ∅ ) = ∅ )
28	27	simpli	⊢ 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 )
29	28	a1i	⊢ ( ⊤ → 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
30	18 19 20 21 25 29	fucoridid	⊢ ( ⊤ → ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) = 𝑁 )
31	30	mptru	⊢ ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) = 𝑁
32	31	fveq1i	⊢ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ( 𝑁 ‘ ∅ )
33	27	simpri	⊢ ( 𝑁 ‘ ∅ ) = ∅
34	32 33	eqtri	⊢ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ∅
35	2	par2catid	⊢ ( 𝐸 ∈ Cat ∧ ( Id ‘ 𝐸 ) = ( 𝑦 ∈ 2_o ↦ 2_o ) )
36	35	simpli	⊢ 𝐸 ∈ Cat
37	36	a1i	⊢ ( ⊤ → 𝐸 ∈ Cat )
38	2 5 6	parswapfunc	⊢ ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ ∈ ( 𝐸 Func 𝐸 )
39	7 38	eqeltri	⊢ 𝑆 ∈ ( 𝐸 Func 𝐸 )
40	39	a1i	⊢ ( ⊤ → 𝑆 ∈ ( 𝐸 Func 𝐸 ) )
41		mptresid	⊢ ( I ↾ 2_o ) = ( 𝑥 ∈ 2_o ↦ 𝑥 )
42		2oex	⊢ 2_o ∈ V
43	42	mptex	⊢ ( 𝑥 ∈ 2_o ↦ 𝑥 ) ∈ V
44	41 43	eqeltri	⊢ ( I ↾ 2_o ) ∈ V
45	42 42	mpoex	⊢ ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) ∈ V
46	6 45	eqeltri	⊢ 𝑀 ∈ V
47	44 46	op1std	⊢ ( 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ → ( 1^st ‘ 𝑆 ) = ( I ↾ 2_o ) )
48	7 47	mp1i	⊢ ( ⊤ → ( 1^st ‘ 𝑆 ) = ( I ↾ 2_o ) )
49	24 3 8 9 10 40 48	termcpostfix	⊢ ( ⊤ → ( 𝐾 ∈ ( 𝑄 Func 𝑄 ) ∧ ( 1^st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐸 ) ) ) )
50	49	simpld	⊢ ( ⊤ → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
51	26	simp1i	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
52	51	simpli	⊢ 𝐹 ∈ ( 𝐶 Func 𝐸 )
53	52	a1i	⊢ ( ⊤ → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
54	51	simpri	⊢ 𝐺 ∈ ( 𝐶 Func 𝐸 )
55	54	a1i	⊢ ( ⊤ → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
56	3 4 25 37 50 53 55 29 21 20	fucoaltval	⊢ ( ⊤ → ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) = ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) )
57	56	mptru	⊢ ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) = ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 )
58	57	fveq1i	⊢ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ )
59		0lt1o	⊢ ∅ ∈ 1_o
60	1	setc1obas	⊢ 1_o = ( Base ‘ 𝐶 )
61	59 60	eleqtri	⊢ ∅ ∈ ( Base ‘ 𝐶 )
62	61	a1i	⊢ ( ⊤ → ∅ ∈ ( Base ‘ 𝐶 ) )
63	3 8 9 40 25 10 53 55 29 62	postcof2	⊢ ( ⊤ → ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) ) )
64	63	mptru	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) )
65	26	simp3i	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o )
66	65	simpli	⊢ ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅
67	65	simpri	⊢ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o
68	44 46	op2ndd	⊢ ( 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ → ( 2^nd ‘ 𝑆 ) = 𝑀 )
69	7 68	ax-mp	⊢ ( 2^nd ‘ 𝑆 ) = 𝑀
70	66 67 69	oveq123i	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) = ( ∅ 𝑀 1_o )
71	70 33	fveq12i	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) ) = ( ( ∅ 𝑀 1_o ) ‘ ∅ )
72	64 71	eqtri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ∅ 𝑀 1_o ) ‘ ∅ )
73		0ex	⊢ ∅ ∈ V
74	73	prid1	⊢ ∅ ∈ { ∅ , 1_o }
75		df2o3	⊢ 2_o = { ∅ , 1_o }
76	74 75	eleqtrri	⊢ ∅ ∈ 2_o
77	76	a1i	⊢ ( ⊤ → ∅ ∈ 2_o )
78		1oelpr	⊢ 1_o ∈ { ∅ , 1_o }
79	78 75	eleqtrri	⊢ 1_o ∈ 2_o
80	79	a1i	⊢ ( ⊤ → 1_o ∈ 2_o )
81		eqid	⊢ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) = ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) )
82	81	par2hom	⊢ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = { 2_o } ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = { 2_o } ∧ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = ∅ ) )
83	82	simp3i	⊢ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = ∅ )
84	83	simpli	⊢ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o
85	76 84	eleqtrri	⊢ ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o )
86	85	a1i	⊢ ( ⊤ → ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) )
87	6 77 80 86	fvmpomptd	⊢ ( ⊤ → ( ( ∅ 𝑀 1_o ) ‘ ∅ ) = ( 𝐴 ‘ ∅ ) )
88	87	mptru	⊢ ( ( ∅ 𝑀 1_o ) ‘ ∅ ) = ( 𝐴 ‘ ∅ )
89	5	parswapprop	⊢ ( ( 𝐴 ‘ 2_o ) = 2_o ∧ ∀ 𝑡 ∈ 2_o ( 𝐴 ‘ 𝑡 ) ∈ 2_o ∧ ( 𝐴 ‘ ∅ ) = 1_o )
90	89	simp3i	⊢ ( 𝐴 ‘ ∅ ) = 1_o
91	72 88 90	3eqtri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = 1_o
92	58 91	eqtri	⊢ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = 1_o
93	34 92	pm3.2i	⊢ ( ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ∅ ∧ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = 1_o )

Metamath Proof Explorer

Theorem fuconuniqvalslem

Proof