Theorem 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	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		par2cat	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\in \mathrm{Cat}$$
2		eqid	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)=\mathrm{SetCat}\left(1_{𝑜}\right)$$
3		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
4		eqid	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
5		eqid	Could not format ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) = ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) : No typesetting found for |- ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) = ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) with typecode |-
6		eqid	$$⊢\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)\right)=\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)\right)$$
7	2 3 4 5 6	fuconuniq2	Could not format E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) : No typesetting found for |- E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) with typecode |-
8		oveq2	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) = ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) = ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) with typecode |-
9	8	fveq2d	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) = ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) with typecode |-
10		oveq2	$$⊢e=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\to \mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}e=\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
11	10	oveq1d	$$⊢e=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\to \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)=\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\right){\times }_c\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\mathrm{SetCat}\left(1_{𝑜}\right)\right)$$
12	11 10	oveq12d	$$⊢e=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\to \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)=\left(\left(\mathrm{SetCat}\left(1_{𝑜}\right)\mathrm{FuncCat}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\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}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\right)$$
13		eqidd	$$⊢e=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}\to z=z$$
14	9 12 13	breq123d	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z <-> ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) ( ( ( ( SetCat ` 1o ) FuncCat e ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat e ) ) z <-> ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z ) ) with typecode |-
15	8	fveq2d	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) = ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) with typecode |-
16	15	neeq2d	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F e ) ) <-> z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) with typecode |-
17	14 16	anbi12d	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( ( ( 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 ) ) ) <-> ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( ( ( 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 ) ) ) <-> ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) ) with typecode |-
18	17	exbidv	Could not format ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 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. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) ) : No typesetting found for |- ( e = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } -> ( 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. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) ) with typecode |-
19	18	rspcev	Could not format ( ( { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } e. Cat /\ E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) -> 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 |- ( ( { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } e. Cat /\ E. z ( ( 1st ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ( ( ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) Xc. ( ( SetCat ` 1o ) FuncCat ( SetCat ` 1o ) ) ) Func ( ( SetCat ` 1o ) FuncCat { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) z /\ z =/= ( 2nd ` ( <. ( SetCat ` 1o ) , ( SetCat ` 1o ) >. o.F { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. } ) ) ) ) -> 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 |-
20	1 7 19	mp2an	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 |-