Metamath Proof Explorer

Theorem fuconuniqvals

Description: At the same natural-transformation/identity input, the canonical and alternative morphism maps give respectively (/) and 1o at the unique source object (/) . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

		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 × { ∅ } )
	Assertion	fuconuniqvals	⊢ ( ( ( 𝑁 ( ⟨ 𝐹 , ( 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		eqid	⊢ ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) ) = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	fuconuniqvalslem	⊢ ( ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = ∅ ∧ ( ( 𝑁 ( ⟨ 𝐹 , ( id_func ‘ 𝐶 ) ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , ( id_func ‘ 𝐶 ) ⟩ ) ( ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) ‘ ( id_func ‘ 𝐶 ) ) ) ‘ ∅ ) = 1_o )