fuconuniq

Description: The arrow map A fixes the identity arrow 2o and exchanges the two nonidentity parallel arrows (/) and 1o . It gives a concrete alternative to functor composition with the same object function and a different morphism function. All hypotheses name explicit constructed sets; no category or functor existence is assumed. (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 ‘ ⚬ ) ‘ 𝑆 )
	fuconuniq.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
Assertion	fuconuniq	⊢ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

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		fuconuniq.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
12		eqid	⊢ ( 𝐸 Δ_func 𝐶 ) = ( 𝐸 Δ_func 𝐶 )
13		eqid	⊢ ( ( 1^st ‘ ( 𝐸 Δ_func 𝐶 ) ) ‘ ∅ ) = ( ( 1^st ‘ ( 𝐸 Δ_func 𝐶 ) ) ‘ ∅ )
14		eqid	⊢ ( ( 1^st ‘ ( 𝐸 Δ_func 𝐶 ) ) ‘ 1_o ) = ( ( 1^st ‘ ( 𝐸 Δ_func 𝐶 ) ) ‘ 1_o )
15		eqid	⊢ ( 1_o × { ∅ } ) = ( 1_o × { ∅ } )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	fuconuniqlem	⊢ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem fuconuniq

Proof