fuconuniqex

Description: The object function of functor composition does not in general determine its morphism function, even when both source categories are the trivial category. The witness category is the explicit two-object, two-parallel-arrow category of par2cat . (Contributed by Zhi Wang, 14-Sep-2026)

		Ref	Expression
	Assertion	fuconuniqex	⊢ ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		par2cat	⊢ { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ∈ Cat
2		eqid	⊢ ( SetCat ‘ 1_o ) = ( SetCat ‘ 1_o )
3		eqid	⊢ { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
4		eqid	⊢ ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) = ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } )
5		eqid	⊢ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) = ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } )
6		eqid	⊢ ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) = ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) )
7	2 3 4 5 6	fuconuniq2	⊢ ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) )
8		oveq2	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) = ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) )
9	8	fveq2d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) = ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) )
10		oveq2	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) = ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) )
11	10	oveq1d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) = ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) )
12	11 10	oveq12d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) = ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) )
13		eqidd	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → 𝑧 = 𝑧 )
14	9 12 13	breq123d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ↔ ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) 𝑧 ) )
15	8	fveq2d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) = ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) )
16	15	neeq2d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ↔ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ) )
17	14 16	anbi12d	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ) ↔ ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ) ) )
18	17	exbidv	⊢ ( 𝑒 = { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } → ( ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ) ↔ ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ) ) )
19	18	rspcev	⊢ ( ( { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ∈ Cat ∧ ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F { ⟨ ( 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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ } ) ) ) ) → ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ) )
20	1 7 19	mp2an	⊢ ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1^st ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) ( ( ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ×_c ( ( SetCat ‘ 1_o ) FuncCat ( SetCat ‘ 1_o ) ) ) Func ( ( SetCat ‘ 1_o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2^nd ‘ ( ⟨ ( SetCat ‘ 1_o ) , ( SetCat ‘ 1_o ) ⟩ ∘_F 𝑒 ) ) )

Metamath Proof Explorer

Theorem fuconuniqex

Proof