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 
|- E. c e. Cat E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) )

Proof

Step Hyp Ref Expression
1 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
2 termcthin 
 |-  ( ( SetCat ` 1o ) e. TermCat -> ( SetCat ` 1o ) e. ThinCat )
3 thinccat 
 |-  ( ( SetCat ` 1o ) e. ThinCat -> ( SetCat ` 1o ) e. Cat )
4 1 2 3 mp2b 
 |-  ( SetCat ` 1o ) e. Cat
5 fuconuniqex 
 |-  E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) )
6 opeq2 
 |-  ( d = ( SetCat ` 1o ) -> <. ( SetCat ` 1o ) , d >. = <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. )
7 6 fvoveq1d 
 |-  ( d = ( SetCat ` 1o ) -> ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) )
8 oveq1 
 |-  ( d = ( SetCat ` 1o ) -> ( d FuncCat e ) = ( ( SetCat ` 1o ) FuncCat e ) )
9 oveq2 
 |-  ( d = ( SetCat ` 1o ) -> ( ( SetCat ` 1o ) FuncCat d ) = ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) )
10 8 9 oveq12d 
 |-  ( d = ( SetCat ` 1o ) -> ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) = ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) )
11 10 oveq1d 
 |-  ( d = ( SetCat ` 1o ) -> ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) = ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) )
12 eqidd 
 |-  ( d = ( SetCat ` 1o ) -> z = z )
13 7 11 12 breq123d 
 |-  ( d = ( SetCat ` 1o ) -> ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z <-> ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z ) )
14 6 fvoveq1d 
 |-  ( d = ( SetCat ` 1o ) -> ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) )
15 14 neeq2d 
 |-  ( d = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) )
16 13 15 anbi12d 
 |-  ( d = ( SetCat ` 1o ) -> ( ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) <-> ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) )
17 16 exbidv 
 |-  ( d = ( SetCat ` 1o ) -> ( E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) <-> E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) )
18 17 rexbidv 
 |-  ( d = ( SetCat ` 1o ) -> ( E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) <-> E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) )
19 18 rspcev 
 |-  ( ( ( SetCat ` 1o ) e. Cat /\ E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) -> E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) )
20 4 5 19 mp2an 
 |-  E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) )
21 opeq1 
 |-  ( c = ( SetCat ` 1o ) -> <. c , d >. = <. ( SetCat ` 1o ) , d >. )
22 21 fvoveq1d 
 |-  ( c = ( SetCat ` 1o ) -> ( 1st ` ( <. c , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) )
23 oveq1 
 |-  ( c = ( SetCat ` 1o ) -> ( c FuncCat d ) = ( ( SetCat ` 1o ) FuncCat d ) )
24 23 oveq2d 
 |-  ( c = ( SetCat ` 1o ) -> ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) = ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) )
25 oveq1 
 |-  ( c = ( SetCat ` 1o ) -> ( c FuncCat e ) = ( ( SetCat ` 1o ) FuncCat e ) )
26 24 25 oveq12d 
 |-  ( c = ( SetCat ` 1o ) -> ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) = ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) )
27 eqidd 
 |-  ( c = ( SetCat ` 1o ) -> z = z )
28 22 26 27 breq123d 
 |-  ( c = ( SetCat ` 1o ) -> ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z <-> ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z ) )
29 21 fvoveq1d 
 |-  ( c = ( SetCat ` 1o ) -> ( 2nd ` ( <. c , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) )
30 29 neeq2d 
 |-  ( c = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. c , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) )
31 28 30 anbi12d 
 |-  ( c = ( SetCat ` 1o ) -> ( ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) ) <-> ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) )
32 31 exbidv 
 |-  ( c = ( SetCat ` 1o ) -> ( E. z ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) ) <-> E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) )
33 32 2rexbidv 
 |-  ( c = ( SetCat ` 1o ) -> ( E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) ) <-> E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) )
34 33 rspcev 
 |-  ( ( ( SetCat ` 1o ) e. Cat /\ E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat d ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) -> E. c e. Cat E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) ) )
35 4 20 34 mp2an 
 |-  E. c e. Cat E. d e. Cat E. e e. Cat E. z ( ( 1st ` ( <. c , d >. o.F e ) ) ( ( ( d FuncCat e ) Xc. ( c FuncCat d ) ) Func ( c FuncCat e ) ) z /\ z =/= ( 2nd ` ( <. c , d >. o.F e ) ) )