Theorem relfunc

Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	relfunc	|- Rel ( D Func E )

Proof

Step	Hyp	Ref	Expression
1		df-func	|- Func = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
2	1	relmpoopab	|- Rel ( D Func E )