Metamath Proof Explorer

Theorem fuconuniqex2

Description: There are categories for which the object function of functor composition does not determine its morphism function. Choose both source categories to be the trivial category and apply fuconuniqex . The full compatibility conditions are given in fucoisfunc ; fucoisfunc2 expands the natural-transformation component conditions. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Assertion fuconuniqex2 ∃ 𝑐 ∈ Cat ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) )

Proof

Step Hyp Ref Expression
1 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
2 termcthin ⊢ ( ( SetCat ‘ 1o ) ∈ TermCat → ( SetCat ‘ 1o ) ∈ ThinCat )
3 thinccat ⊢ ( ( SetCat ‘ 1o ) ∈ ThinCat → ( SetCat ‘ 1o ) ∈ Cat )
4 1 2 3 mp2b ⊢ ( SetCat ‘ 1o ) ∈ Cat
5 fuconuniqex ⊢ ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) )
6 opeq2 ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ = ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ )
7 6 fvoveq1d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) = ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) )
8 oveq1 ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 𝑑 FuncCat 𝑒 ) = ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) )
9 oveq2 ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) = ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) )
10 8 9 oveq12d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) = ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) )
11 10 oveq1d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) = ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) )
12 eqidd ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → 𝑧 = 𝑧 )
13 7 11 12 breq123d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ↔ ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ) )
14 6 fvoveq1d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) = ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) )
15 14 neeq2d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ↔ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ) )
16 13 15 anbi12d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ) ) )
17 16 exbidv ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ) ) )
18 17 rexbidv ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ) ) )
19 18 rspcev ⊢ ( ( ( SetCat ‘ 1o ) ∈ Cat ∧ ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ( ( ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat ( SetCat ‘ 1o ) ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , ( SetCat ‘ 1o ) ⟩ ∘F 𝑒 ) ) ) ) → ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) )
20 4 5 19 mp2an ⊢ ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) )
21 opeq1 ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ )
22 21 fvoveq1d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) = ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) )
23 oveq1 ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( 𝑐 FuncCat 𝑑 ) = ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) )
24 23 oveq2d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) = ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) )
25 oveq1 ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( 𝑐 FuncCat 𝑒 ) = ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) )
26 24 25 oveq12d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) = ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) )
27 eqidd ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → 𝑧 = 𝑧 )
28 22 26 27 breq123d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ↔ ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ) )
29 21 fvoveq1d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) = ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) )
30 29 neeq2d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ↔ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) )
31 28 30 anbi12d ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ) )
32 31 exbidv ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ∃ 𝑧 ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ) )
33 32 2rexbidv ⊢ ( 𝑐 = ( SetCat ‘ 1o ) → ( ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ) ↔ ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ) )
34 33 rspcev ⊢ ( ( ( SetCat ‘ 1o ) ∈ Cat ∧ ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( ( SetCat ‘ 1o ) FuncCat 𝑑 ) ) Func ( ( SetCat ‘ 1o ) FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ ( SetCat ‘ 1o ) , 𝑑 ⟩ ∘F 𝑒 ) ) ) ) → ∃ 𝑐 ∈ Cat ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ) )
35 4 20 34 mp2an ⊢ ∃ 𝑐 ∈ Cat ∃ 𝑑 ∈ Cat ∃ 𝑒 ∈ Cat ∃ 𝑧 ( ( 1st ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) ( ( ( 𝑑 FuncCat 𝑒 ) ×c ( 𝑐 FuncCat 𝑑 ) ) Func ( 𝑐 FuncCat 𝑒 ) ) 𝑧 ∧ 𝑧 ≠ ( 2nd ‘ ( ⟨ 𝑐 , 𝑑 ⟩ ∘F 𝑒 ) ) )