fuconuniq2

Description: The concrete parallel-arrow category supplies a morphism function different from canonical functor composition, with its object function fixed exactly. See par2cat and par2hom for the category and its four hom-sets. (Contributed by Zhi Wang, 14-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 𝐸 )
	fuconuniq2.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
Assertion	fuconuniq2	⊢ ∃ 𝑧 ( ( 1^st ‘ 𝐿 ) ( 𝑇 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		fuconuniq2.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
6		fvex	⊢ ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ∈ V
7		breq2	⊢ ( 𝑧 = ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) → ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) 𝑧 ↔ ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ) )
8		neeq1	⊢ ( 𝑧 = ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) → ( 𝑧 ≠ ( 2^nd ‘ 𝐿 ) ↔ ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) ) )
9	7 8	anbi12d	⊢ ( 𝑧 = ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) → ( ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ 𝐿 ) ) ↔ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) ) ) )
10		eqid	⊢ ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) = ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) )
11		eqid	⊢ ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) = ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) )
12		eqid	⊢ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ = ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩
13		eqid	⊢ ( 𝐸 FuncCat 𝐸 ) = ( 𝐸 FuncCat 𝐸 )
14		eqid	⊢ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) = ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) )
15		eqid	⊢ ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) = ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ )
16	1 2 3 4 10 11 12 13 14 15 5	fuconuniq	⊢ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( ( ( 1^st ‘ ( ⟨ ( 𝐸 FuncCat 𝐸 ) , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) ) ) ‘ ⟨ ( I ↾ 2_o ) , ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) ) ‘ 𝑎 ) ) ) ⟩ ) ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )
17	6 9 16	ceqsexv2d	⊢ ∃ 𝑧 ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem fuconuniq2

Proof