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	Could not format assertion : No typesetting found for |- 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 ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
2		termcthin	Could not format ( ( SetCat ` 1o ) e. TermCat -> ( SetCat ` 1o ) e. ThinCat ) : No typesetting found for |- ( ( SetCat ` 1o ) e. TermCat -> ( SetCat ` 1o ) e. ThinCat ) with typecode |-
3		thinccat	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)\in \mathrm{ThinCat}\to \mathrm{SetCat}\left(1_{𝑜}\right)\in \mathrm{Cat}$$
4	1 2 3	mp2b	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)\in \mathrm{Cat}$$
5		fuconuniqex	Could not format 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 ) ) ) : No typesetting found for |- 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 ) ) ) with typecode |-
6		opeq2	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to ⟨\mathrm{SetCat}\left(1_{𝑜}\right),d⟩=⟨\mathrm{SetCat}\left(1_{𝑜}\right),\mathrm{SetCat}\left(1_{𝑜}\right)⟩$$
7	6	fvoveq1d	Could not format ( d = ( SetCat ` 1o ) -> ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) : No typesetting found for |- ( d = ( SetCat ` 1o ) -> ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) with typecode |-
8		oveq1	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to d\mathrm{FuncCat}e=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e$$
9		oveq2	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to \mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)$$
10	8 9	oveq12d	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to \left(d\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d\right)=\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)\right)$$
11	10	oveq1d	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to \left(\left(d\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d\right)\right)\mathrm{Func}\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e\right)=\left(\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)\right)\right)\mathrm{Func}\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e\right)$$
12		eqidd	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to z=z$$
13	7 11 12	breq123d	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
14	6	fvoveq1d	Could not format ( d = ( SetCat ` 1o ) -> ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) : No typesetting found for |- ( d = ( SetCat ` 1o ) -> ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) with typecode |-
15	14	neeq2d	Could not format ( d = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) : No typesetting found for |- ( d = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ) ) with typecode |-
16	13 15	anbi12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
17	16	exbidv	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
18	17	rexbidv	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
19	18	rspcev	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
20	4 5 19	mp2an	Could not format 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 ) ) ) : No typesetting found for |- 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 ) ) ) with typecode |-
21		opeq1	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to ⟨c,d⟩=⟨\mathrm{SetCat}\left(1_{𝑜}\right),d⟩$$
22	21	fvoveq1d	Could not format ( c = ( SetCat ` 1o ) -> ( 1st ` ( <. c , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) : No typesetting found for |- ( c = ( SetCat ` 1o ) -> ( 1st ` ( <. c , d >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) with typecode |-
23		oveq1	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to c\mathrm{FuncCat}d=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d$$
24	23	oveq2d	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to \left(d\mathrm{FuncCat}e\right){\times }_c\left(c\mathrm{FuncCat}d\right)=\left(d\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d\right)$$
25		oveq1	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to c\mathrm{FuncCat}e=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e$$
26	24 25	oveq12d	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to \left(\left(d\mathrm{FuncCat}e\right){\times }_c\left(c\mathrm{FuncCat}d\right)\right)\mathrm{Func}\left(c\mathrm{FuncCat}e\right)=\left(\left(d\mathrm{FuncCat}e\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}d\right)\right)\mathrm{Func}\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e\right)$$
27		eqidd	$$⊢c=\mathrm{SetCat}\left(1_{𝑜}\right)\to z=z$$
28	22 26 27	breq123d	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
29	21	fvoveq1d	Could not format ( c = ( SetCat ` 1o ) -> ( 2nd ` ( <. c , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) : No typesetting found for |- ( c = ( SetCat ` 1o ) -> ( 2nd ` ( <. c , d >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) with typecode |-
30	29	neeq2d	Could not format ( c = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. c , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) : No typesetting found for |- ( c = ( SetCat ` 1o ) -> ( z =/= ( 2nd ` ( <. c , d >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , d >. o.F e ) ) ) ) with typecode |-
31	28 30	anbi12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
32	31	exbidv	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
33	32	2rexbidv	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
34	33	rspcev	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
35	4 20 34	mp2an	Could not format 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 ) ) ) : No typesetting found for |- 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 ) ) ) with typecode |-