Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  setiscat Unicode version

Theorem setiscat 25979
Description: The category set is a category. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
setiscat  |-  ( U  e.  Univ  ->  ( SetCat OLD `  U )  e.  Cat OLD  )

Proof of Theorem setiscat
Dummy variables  f 
g  h  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscatset 25978 . 2  |-  ( U  e.  Univ  ->  ( SetCat OLD `  U )  =  <. <.
( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >. )
2 domcatfun 25925 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( dom SetCat `
 U ) : ( Morphism SetCat `  U ) --> U )
3 domdomcatfun 25926 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  dom  ( dom
SetCat `  U )  =  ( Morphism SetCat `  U )
)
4 domidcat 25945 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  dom  ( Id SetCat `  U )  =  U )
53, 4feq23d 5386 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( dom SetCat `  U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U )  <->  ( dom SetCat `  U ) : (
Morphism
SetCat `  U ) --> U ) )
62, 5mpbird 223 . . . . . . . 8  |-  ( U  e.  Univ  ->  ( dom SetCat `
 U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U ) )
7 codcatfun 25934 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( cod SetCat `
 U ) : ( Morphism SetCat `  U ) --> U )
83, 4feq23d 5386 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( cod SetCat `  U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U )  <->  ( cod SetCat `  U ) : (
Morphism
SetCat `  U ) --> U ) )
97, 8mpbird 223 . . . . . . . 8  |-  ( U  e.  Univ  ->  ( cod SetCat `
 U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U ) )
10 idcatfun 25941 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( Id SetCat `
 U ) : U --> ( Morphism SetCat `  U
) )
114, 3feq23d 5386 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( Id SetCat `  U ) : dom  ( Id SetCat `  U ) --> dom  ( dom
SetCat `  U )  <->  ( Id SetCat `  U ) : U --> ( Morphism SetCat `  U )
) )
1210, 11mpbird 223 . . . . . . . 8  |-  ( U  e.  Univ  ->  ( Id SetCat `
 U ) : dom  ( Id SetCat `  U ) --> dom  ( dom
SetCat `  U ) )
136, 9, 123jca 1132 . . . . . . 7  |-  ( U  e.  Univ  ->  ( ( dom SetCat `  U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U )  /\  ( cod
SetCat `  U ) : dom  ( dom SetCat `  U
) --> dom  ( Id SetCat `  U )  /\  ( Id SetCat `  U ) : dom  ( Id SetCat `  U ) --> dom  ( dom
SetCat `  U ) ) )
14 cmpmorfun 25971 . . . . . . . 8  |-  ( U  e.  Univ  ->  Fun  ( ro SetCat `  U )
)
15 cmppar 25973 . . . . . . . . 9  |-  ( U  e.  Univ  ->  dom  ( ro SetCat `  U )  C_  ( ( Morphism SetCat `  U
)  X.  ( Morphism SetCat `  U ) ) )
163, 3xpeq12d 4714 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( dom  ( dom SetCat `  U
)  X.  dom  ( dom
SetCat `  U ) )  =  ( ( Morphism SetCat `  U )  X.  ( Morphism SetCat `  U ) ) )
1715, 16sseqtr4d 3215 . . . . . . . 8  |-  ( U  e.  Univ  ->  dom  ( ro SetCat `  U )  C_  ( dom  ( dom SetCat `
 U )  X. 
dom  ( dom SetCat `  U
) ) )
18 cmpmor 25975 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ran  ( ro SetCat `  U )  C_  ( Morphism SetCat `  U )
)
1918, 3sseqtr4d 3215 . . . . . . . 8  |-  ( U  e.  Univ  ->  ran  ( ro SetCat `  U )  C_ 
dom  ( dom SetCat `  U
) )
2014, 17, 193jca 1132 . . . . . . 7  |-  ( U  e.  Univ  ->  ( Fun  ( ro SetCat `  U
)  /\  dom  ( ro SetCat `
 U )  C_  ( dom  ( dom SetCat `  U
)  X.  dom  ( dom
SetCat `  U ) )  /\  ran  ( ro SetCat `
 U )  C_  dom  ( dom SetCat `  U
) ) )
21 fvex 5539 . . . . . . . . . 10  |-  ( dom SetCat `
 U )  e. 
_V
22 fvex 5539 . . . . . . . . . 10  |-  ( cod SetCat `
 U )  e. 
_V
23 fvex 5539 . . . . . . . . . 10  |-  ( Id SetCat `
 U )  e. 
_V
2421, 22, 233pm3.2i 1130 . . . . . . . . 9  |-  ( ( dom SetCat `  U )  e.  _V  /\  ( cod SetCat `
 U )  e. 
_V  /\  ( Id SetCat `  U )  e.  _V )
25 fvex 5539 . . . . . . . . 9  |-  ( ro SetCat `
 U )  e. 
_V
2624, 25pm3.2i 441 . . . . . . . 8  |-  ( ( ( dom SetCat `  U
)  e.  _V  /\  ( cod SetCat `  U )  e.  _V  /\  ( Id SetCat `
 U )  e. 
_V )  /\  ( ro SetCat `  U )  e.  _V )
27 eqid 2283 . . . . . . . . 9  |-  dom  ( dom
SetCat `  U )  =  dom  ( dom SetCat `  U
)
28 eqid 2283 . . . . . . . . 9  |-  dom  ( Id SetCat `  U )  =  dom  ( Id SetCat `  U )
2927, 28isalg 25721 . . . . . . . 8  |-  ( ( ( ( dom SetCat `  U
)  e.  _V  /\  ( cod SetCat `  U )  e.  _V  /\  ( Id SetCat `
 U )  e. 
_V )  /\  ( ro SetCat `  U )  e.  _V )  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  <->  ( (
( dom SetCat `  U
) : dom  ( dom
SetCat `  U ) --> dom  ( Id SetCat `  U
)  /\  ( cod SetCat `  U ) : dom  ( dom SetCat `  U ) --> dom  ( Id SetCat `  U
)  /\  ( Id SetCat `  U ) : dom  ( Id SetCat `  U ) --> dom  ( dom SetCat `  U
) )  /\  ( Fun  ( ro SetCat `  U
)  /\  dom  ( ro SetCat `
 U )  C_  ( dom  ( dom SetCat `  U
)  X.  dom  ( dom
SetCat `  U ) )  /\  ran  ( ro SetCat `
 U )  C_  dom  ( dom SetCat `  U
) ) ) ) )
3026, 29mp1i 11 . . . . . . 7  |-  ( U  e.  Univ  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  <->  ( (
( dom SetCat `  U
) : dom  ( dom
SetCat `  U ) --> dom  ( Id SetCat `  U
)  /\  ( cod SetCat `  U ) : dom  ( dom SetCat `  U ) --> dom  ( Id SetCat `  U
)  /\  ( Id SetCat `  U ) : dom  ( Id SetCat `  U ) --> dom  ( dom SetCat `  U
) )  /\  ( Fun  ( ro SetCat `  U
)  /\  dom  ( ro SetCat `
 U )  C_  ( dom  ( dom SetCat `  U
)  X.  dom  ( dom
SetCat `  U ) )  /\  ran  ( ro SetCat `
 U )  C_  dom  ( dom SetCat `  U
) ) ) ) )
3113, 20, 30mpbir2and 888 . . . . . 6  |-  ( U  e.  Univ  ->  <. <. ( dom
SetCat `  U ) ,  ( cod SetCat `  U
) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  )
324eleq2d 2350 . . . . . . . . . . 11  |-  ( U  e.  Univ  ->  ( a  e.  dom  ( Id SetCat `
 U )  <->  a  e.  U ) )
3332biimpd 198 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  ( a  e.  dom  ( Id SetCat `
 U )  -> 
a  e.  U ) )
3433imdistani 671 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  a  e.  dom  ( Id SetCat `  U ) )  -> 
( U  e.  Univ  /\  a  e.  U ) )
35 domidmor 25948 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  a  e.  U )  ->  (
( dom SetCat `  U
) `  ( ( Id SetCat `  U ) `  a ) )  =  a )
3634, 35syl 15 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  a  e.  dom  ( Id SetCat `  U ) )  -> 
( ( dom SetCat `  U
) `  ( ( Id SetCat `  U ) `  a ) )  =  a )
37 codidmor 25950 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  a  e.  U )  ->  (
( cod SetCat `  U
) `  ( ( Id SetCat `  U ) `  a ) )  =  a )
3834, 37syl 15 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  a  e.  dom  ( Id SetCat `  U ) )  -> 
( ( cod SetCat `  U
) `  ( ( Id SetCat `  U ) `  a ) )  =  a )
3936, 38jca 518 . . . . . . 7  |-  ( ( U  e.  Univ  /\  a  e.  dom  ( Id SetCat `  U ) )  -> 
( ( ( dom SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a  /\  ( ( cod SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a ) )
4039ralrimiva 2626 . . . . . 6  |-  ( U  e.  Univ  ->  A. a  e.  dom  ( Id SetCat `  U ) ( ( ( dom SetCat `  U
) `  ( ( Id SetCat `  U ) `  a ) )  =  a  /\  ( ( cod SetCat `  U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a ) )
41 simpl 443 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  U  e.  Univ )
42 simprr 733 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  g  e.  dom  ( dom SetCat `  U
) )
43 simprl 732 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  f  e.  dom  ( dom SetCat `  U
) )
4441, 42, 433jca 1132 . . . . . . . . . . . 12  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( U  e.  Univ  /\  g  e.  dom  ( dom SetCat `  U
)  /\  f  e.  dom  ( dom SetCat `  U
) ) )
45 eleq2 2344 . . . . . . . . . . . . 13  |-  ( (
Morphism
SetCat `  U )  =  dom  ( dom SetCat `  U
)  ->  ( g  e.  ( Morphism SetCat `  U )  <->  g  e.  dom  ( dom SetCat `
 U ) ) )
46 eleq2 2344 . . . . . . . . . . . . 13  |-  ( (
Morphism
SetCat `  U )  =  dom  ( dom SetCat `  U
)  ->  ( f  e.  ( Morphism SetCat `  U )  <->  f  e.  dom  ( dom SetCat `
 U ) ) )
4745, 463anbi23d 1255 . . . . . . . . . . . 12  |-  ( (
Morphism
SetCat `  U )  =  dom  ( dom SetCat `  U
)  ->  ( ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) )  <->  ( U  e.  Univ  /\  g  e.  dom  ( dom SetCat `  U
)  /\  f  e.  dom  ( dom SetCat `  U
) ) ) )
4844, 47syl5ibr 212 . . . . . . . . . . 11  |-  ( (
Morphism
SetCat `  U )  =  dom  ( dom SetCat `  U
)  ->  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) ) ) )
4948eqcoms 2286 . . . . . . . . . 10  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  ->  ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) ) ) )
503, 49syl 15 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) ) ) )
5150anabsi5 790 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) ) )
52 cmppar3 25974 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U ) )  -> 
( <. g ,  f
>.  e.  dom  ( ro SetCat `
 U )  <->  ( ( dom
SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )
) )
5351, 52syl 15 . . . . . . 7  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( <. g ,  f >.  e.  dom  ( ro SetCat `  U )  <->  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )
5453ralrimivva 2635 . . . . . 6  |-  ( U  e.  Univ  ->  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( <. g ,  f >.  e.  dom  ( ro SetCat `  U )  <->  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )
5531, 40, 543jca 1132 . . . . 5  |-  ( U  e.  Univ  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  /\  A. a  e.  dom  ( Id SetCat `  U )
( ( ( dom SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a  /\  ( ( cod SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a )  /\  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( <. g ,  f >.  e.  dom  ( ro SetCat `  U )  <->  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) ) )
56 eqid 2283 . . . . . . . . . . . 12  |-  ( ro SetCat `
 U )  =  ( ro SetCat `  U
)
57 eqid 2283 . . . . . . . . . . . 12  |-  ( Morphism SetCat `  U )  =  (
Morphism
SetCat `  U )
58 eqid 2283 . . . . . . . . . . . 12  |-  ( dom SetCat `
 U )  =  ( dom SetCat `  U
)
59 eqid 2283 . . . . . . . . . . . 12  |-  ( cod SetCat `
 U )  =  ( cod SetCat `  U
)
6056, 57, 58, 59cmp2morpdom 25964 . . . . . . . . . . 11  |-  ( ( U  e.  Univ  /\  (
g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U )
)  /\  ( ( dom
SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )
)  ->  ( ( dom
SetCat `  U ) `  ( g ( ro SetCat `
 U ) f ) )  =  ( ( dom SetCat `  U
) `  f )
)
61603exp 1150 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  ( ( g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) ) )
6261ancomsd 440 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) ) )
63 eleq2 2344 . . . . . . . . . . 11  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
f  e.  dom  ( dom
SetCat `  U )  <->  f  e.  ( Morphism SetCat `  U )
) )
64 eleq2 2344 . . . . . . . . . . 11  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
g  e.  dom  ( dom
SetCat `  U )  <->  g  e.  ( Morphism SetCat `  U )
) )
6563, 64anbi12d 691 . . . . . . . . . 10  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
)  <->  ( f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U ) ) ) )
6665imbi1d 308 . . . . . . . . 9  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
( ( f  e. 
dom  ( dom SetCat `  U
)  /\  g  e.  dom  ( dom SetCat `  U
) )  ->  (
( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) )  <-> 
( ( f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U ) )  -> 
( ( ( dom SetCat `
 U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) ) ) )
6762, 66syl5ibr 212 . . . . . . . 8  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  ( U  e.  Univ  ->  (
( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) ) ) )
683, 67mpcom 32 . . . . . . 7  |-  ( U  e.  Univ  ->  ( ( f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) )  ->  ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) ) )
6968ralrimivv 2634 . . . . . 6  |-  ( U  e.  Univ  ->  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) ) )
7056, 57, 58, 59cmp2morpcod 25965 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  (
g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U )
)  /\  ( ( dom
SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )
)  ->  ( ( cod
SetCat `  U ) `  ( g ( ro SetCat `
 U ) f ) )  =  ( ( cod SetCat `  U
) `  g )
)
71703exp 1150 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  ( ( g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) )
7271com12 27 . . . . . . . . . . 11  |-  ( ( g  e.  ( Morphism SetCat `  U )  /\  f  e.  ( Morphism SetCat `  U )
)  ->  ( U  e.  Univ  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) )
7372ancoms 439 . . . . . . . . . 10  |-  ( ( f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U )
)  ->  ( U  e.  Univ  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) )
7465, 73syl6bi 219 . . . . . . . . 9  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  (
( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
)  ->  ( U  e.  Univ  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) ) )
7574com23 72 . . . . . . . 8  |-  ( dom  ( dom SetCat `  U
)  =  ( Morphism SetCat `  U )  ->  ( U  e.  Univ  ->  (
( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) ) )
763, 75mpcom 32 . . . . . . 7  |-  ( U  e.  Univ  ->  ( ( f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) )  ->  ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) )
7776ralrimivv 2634 . . . . . 6  |-  ( U  e.  Univ  ->  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) )
7869, 77jca 518 . . . . 5  |-  ( U  e.  Univ  ->  ( A. f  e.  dom  ( dom SetCat `
 U ) A. g  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) )  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) )
7927, 28isded 25736 . . . . . 6  |-  ( ( ( ( dom SetCat `  U
)  e.  _V  /\  ( cod SetCat `  U )  e.  _V  /\  ( Id SetCat `
 U )  e. 
_V )  /\  ( ro SetCat `  U )  e.  _V )  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded  <->  ( ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  /\  A. a  e.  dom  ( Id SetCat `  U )
( ( ( dom SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a  /\  ( ( cod SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a )  /\  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( <. g ,  f >.  e.  dom  ( ro SetCat `  U )  <->  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  /\  ( A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) )  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) ) ) )
8026, 79mp1i 11 . . . . 5  |-  ( U  e.  Univ  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded  <->  ( ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Alg  /\  A. a  e.  dom  ( Id SetCat `  U )
( ( ( dom SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a  /\  ( ( cod SetCat `
 U ) `  ( ( Id SetCat `  U ) `  a
) )  =  a )  /\  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( <. g ,  f >.  e.  dom  ( ro SetCat `  U )  <->  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  /\  ( A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) ( ( ( dom SetCat `  U ) `  g )  =  ( ( cod SetCat `  U
) `  f )  ->  ( ( dom SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( dom SetCat `
 U ) `  f ) )  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( cod SetCat `  U
) `  ( g
( ro SetCat `  U
) f ) )  =  ( ( cod SetCat `
 U ) `  g ) ) ) ) ) )
8155, 78, 80mpbir2and 888 . . . 4  |-  ( U  e.  Univ  ->  <. <. ( dom
SetCat `  U ) ,  ( cod SetCat `  U
) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded )
82 simp1l 979 . . . . . . . 8  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
)  /\  ( (
( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  ->  U  e.  Univ )
833eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( U  e.  Univ  ->  ( f  e.  dom  ( dom SetCat `
 U )  <->  f  e.  ( Morphism SetCat `  U )
) )
8483biimpd 198 . . . . . . . . . . . . 13  |-  ( U  e.  Univ  ->  ( f  e.  dom  ( dom SetCat `
 U )  -> 
f  e.  ( Morphism SetCat `  U ) ) )
8584adantrd 454 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  ( ( f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) )  ->  f  e.  (
Morphism
SetCat `  U ) ) )
8685imp 418 . . . . . . . . . . 11  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  f  e.  ( Morphism SetCat `  U )
)
8786adantr 451 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
) )  ->  f  e.  ( Morphism SetCat `  U )
)
883eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( U  e.  Univ  ->  ( g  e.  dom  ( dom SetCat `
 U )  <->  g  e.  ( Morphism SetCat `  U )
) )
8988biimpd 198 . . . . . . . . . . . . 13  |-  ( U  e.  Univ  ->  ( g  e.  dom  ( dom SetCat `
 U )  -> 
g  e.  ( Morphism SetCat `  U ) ) )
9089adantld 453 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  ( ( f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) )  ->  g  e.  (
Morphism
SetCat `  U ) ) )
9190imp 418 . . . . . . . . . . 11  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  g  e.  ( Morphism SetCat `  U )
)
9291adantr 451 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
) )  ->  g  e.  ( Morphism SetCat `  U )
)
933eleq2d 2350 . . . . . . . . . . . . 13  |-  ( U  e.  Univ  ->  ( h  e.  dom  ( dom SetCat `
 U )  <->  h  e.  ( Morphism SetCat `  U )
) )
9493biimpd 198 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  ( h  e.  dom  ( dom SetCat `
 U )  ->  h  e.  ( Morphism SetCat `  U ) ) )
9594adantr 451 . . . . . . . . . . 11  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( h  e.  dom  ( dom SetCat `  U
)  ->  h  e.  ( Morphism SetCat `  U )
) )
9695imp 418 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
) )  ->  h  e.  ( Morphism SetCat `  U )
)
9787, 92, 963jca 1132 . . . . . . . . 9  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
) )  ->  (
f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U )  /\  h  e.  ( Morphism SetCat `  U ) ) )
98973adant3 975 . . . . . . . 8  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
)  /\  ( (
( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  ->  ( f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U )  /\  h  e.  ( Morphism SetCat `  U )
) )
99 simp3 957 . . . . . . . 8  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
)  /\  ( (
( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  ->  ( ( ( dom SetCat `  U ) `  h )  =  ( ( cod SetCat `  U
) `  g )  /\  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )
10056, 57, 58, 59cmpmorass 25966 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  (
f  e.  ( Morphism SetCat `  U )  /\  g  e.  ( Morphism SetCat `  U )  /\  h  e.  ( Morphism SetCat `  U ) )  /\  ( ( ( dom SetCat `
 U ) `  h )  =  ( ( cod SetCat `  U
) `  g )  /\  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  ->  ( h ( ro SetCat `  U )
( g ( ro SetCat `
 U ) f ) )  =  ( ( h ( ro SetCat `
 U ) g ) ( ro SetCat `  U ) f ) )
10182, 98, 99, 100syl3anc 1182 . . . . . . 7  |-  ( ( ( U  e.  Univ  /\  ( f  e.  dom  ( dom SetCat `  U )  /\  g  e.  dom  ( dom SetCat `  U )
) )  /\  h  e.  dom  ( dom SetCat `  U
)  /\  ( (
( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) ) )  ->  ( h ( ro SetCat `  U )
( g ( ro SetCat `
 U ) f ) )  =  ( ( h ( ro SetCat `
 U ) g ) ( ro SetCat `  U ) f ) )
1021013exp 1150 . . . . . 6  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  ( h  e.  dom  ( dom SetCat `  U
)  ->  ( (
( ( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) ) )
103102ralrimiv 2625 . . . . 5  |-  ( ( U  e.  Univ  /\  (
f  e.  dom  ( dom
SetCat `  U )  /\  g  e.  dom  ( dom SetCat `
 U ) ) )  ->  A. h  e.  dom  ( dom SetCat `  U
) ( ( ( ( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) )
104103ralrimivva 2635 . . . 4  |-  ( U  e.  Univ  ->  A. f  e.  dom  ( dom SetCat `  U
) A. g  e. 
dom  ( dom SetCat `  U
) A. h  e. 
dom  ( dom SetCat `  U
) ( ( ( ( dom SetCat `  U
) `  h )  =  ( ( cod SetCat `
 U ) `  g )  /\  (
( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) )
10581, 104jca 518 . . 3  |-  ( U  e.  Univ  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) A. h  e.  dom  ( dom SetCat `
 U ) ( ( ( ( dom SetCat `
 U ) `  h )  =  ( ( cod SetCat `  U
) `  g )  /\  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) ) )
10684adantld 453 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  ( ( ( ( cod SetCat `  U
) `  f )  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  f  e.  ( Morphism SetCat `  U )
) )
107106anc2li 540 . . . . . . . . 9  |-  ( U  e.  Univ  ->  ( ( ( ( cod SetCat `  U
) `  f )  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  ( U  e.  Univ  /\  f  e.  ( Morphism SetCat `  U )
) ) )
108 eqid 2283 . . . . . . . . . 10  |-  ( Id SetCat `
 U )  =  ( Id SetCat `  U
)
10956, 57, 59, 108cmpidmor2 25969 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  f  e.  ( Morphism SetCat `  U )
)  ->  ( (
( Id SetCat `  U
) `  ( ( cod
SetCat `  U ) `  f ) ) ( ro SetCat `  U )
f )  =  f )
110107, 109syl6 29 . . . . . . . 8  |-  ( U  e.  Univ  ->  ( ( ( ( cod SetCat `  U
) `  f )  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  (
( ( Id SetCat `  U ) `  (
( cod SetCat `  U
) `  f )
) ( ro SetCat `  U ) f )  =  f ) )
111 eleq1 2343 . . . . . . . . . 10  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
a  e.  dom  ( Id SetCat `  U )  <->  ( ( cod SetCat `  U
) `  f )  e.  dom  ( Id SetCat `  U ) ) )
112111anbi1d 685 . . . . . . . . 9  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  <->  ( ( ( cod SetCat `  U ) `  f )  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
) ) )
113 fveq2 5525 . . . . . . . . . . 11  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( Id SetCat `  U
) `  a )  =  ( ( Id SetCat `
 U ) `  ( ( cod SetCat `  U
) `  f )
) )
114113oveq1d 5873 . . . . . . . . . 10  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( ( Id SetCat `  U ) `  a
) ( ro SetCat `  U ) f )  =  ( ( ( Id SetCat `  U ) `  ( ( cod SetCat `  U
) `  f )
) ( ro SetCat `  U ) f ) )
115114eqeq1d 2291 . . . . . . . . 9  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( ( ( Id SetCat `
 U ) `  a ) ( ro SetCat `
 U ) f )  =  f  <->  ( (
( Id SetCat `  U
) `  ( ( cod
SetCat `  U ) `  f ) ) ( ro SetCat `  U )
f )  =  f ) )
116112, 115imbi12d 311 . . . . . . . 8  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  (
( ( a  e. 
dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  (
( ( Id SetCat `  U ) `  a
) ( ro SetCat `  U ) f )  =  f )  <->  ( (
( ( cod SetCat `  U
) `  f )  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  (
( ( Id SetCat `  U ) `  (
( cod SetCat `  U
) `  f )
) ( ro SetCat `  U ) f )  =  f ) ) )
117110, 116syl5ibr 212 . . . . . . 7  |-  ( a  =  ( ( cod SetCat `
 U ) `  f )  ->  ( U  e.  Univ  ->  (
( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f ) ) )
118117eqcoms 2286 . . . . . 6  |-  ( ( ( cod SetCat `  U
) `  f )  =  a  ->  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f ) ) )
119118com3l 75 . . . . 5  |-  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( cod SetCat `  U
) `  f )  =  a  ->  ( ( ( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f ) ) )
120119ralrimivv 2634 . . . 4  |-  ( U  e.  Univ  ->  A. a  e.  dom  ( Id SetCat `  U ) A. f  e.  dom  ( dom SetCat `  U
) ( ( ( cod SetCat `  U ) `  f )  =  a  ->  ( ( ( Id SetCat `  U ) `  a ) ( ro SetCat `
 U ) f )  =  f ) )
12184adantld 453 . . . . . . . . . . 11  |-  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  f  e.  ( Morphism SetCat `  U )
) )
122121imdistani 671 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  (
a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
) )  ->  ( U  e.  Univ  /\  f  e.  ( Morphism SetCat `  U )
) )
12356, 57, 58, 108cmpidmor3 25970 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  f  e.  ( Morphism SetCat `  U )
)  ->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  ( ( dom SetCat `  U
) `  f )
) )  =  f )
124122, 123syl 15 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  (
a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
) )  ->  (
f ( ro SetCat `  U ) ( ( Id SetCat `  U ) `  ( ( dom SetCat `  U
) `  f )
) )  =  f )
125124ex 423 . . . . . . . 8  |-  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  ( ( dom SetCat `  U
) `  f )
) )  =  f ) )
126 fveq2 5525 . . . . . . . . . . 11  |-  ( a  =  ( ( dom SetCat `
 U ) `  f )  ->  (
( Id SetCat `  U
) `  a )  =  ( ( Id SetCat `
 U ) `  ( ( dom SetCat `  U
) `  f )
) )
127126oveq2d 5874 . . . . . . . . . 10  |-  ( a  =  ( ( dom SetCat `
 U ) `  f )  ->  (
f ( ro SetCat `  U ) ( ( Id SetCat `  U ) `  a ) )  =  ( f ( ro SetCat `
 U ) ( ( Id SetCat `  U
) `  ( ( dom
SetCat `  U ) `  f ) ) ) )
128127eqeq1d 2291 . . . . . . . . 9  |-  ( a  =  ( ( dom SetCat `
 U ) `  f )  ->  (
( f ( ro SetCat `
 U ) ( ( Id SetCat `  U
) `  a )
)  =  f  <->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  ( ( dom SetCat `  U
) `  f )
) )  =  f ) )
129128imbi2d 307 . . . . . . . 8  |-  ( a  =  ( ( dom SetCat `
 U ) `  f )  ->  (
( ( a  e. 
dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U
) )  ->  (
f ( ro SetCat `  U ) ( ( Id SetCat `  U ) `  a ) )  =  f )  <->  ( (
a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  ( ( dom SetCat `  U
) `  f )
) )  =  f ) ) )
130125, 129syl5ibr 212 . . . . . . 7  |-  ( a  =  ( ( dom SetCat `
 U ) `  f )  ->  ( U  e.  Univ  ->  (
( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) )
131130eqcoms 2286 . . . . . 6  |-  ( ( ( dom SetCat `  U
) `  f )  =  a  ->  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( f
( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) )
132131com3l 75 . . . . 5  |-  ( U  e.  Univ  ->  ( ( a  e.  dom  ( Id SetCat `  U )  /\  f  e.  dom  ( dom SetCat `  U )
)  ->  ( (
( dom SetCat `  U
) `  f )  =  a  ->  ( f ( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) )
133132ralrimivv 2634 . . . 4  |-  ( U  e.  Univ  ->  A. a  e.  dom  ( Id SetCat `  U ) A. f  e.  dom  ( dom SetCat `  U
) ( ( ( dom SetCat `  U ) `  f )  =  a  ->  ( f ( ro SetCat `  U )
( ( Id SetCat `  U ) `  a
) )  =  f ) )
134120, 133jca 518 . . 3  |-  ( U  e.  Univ  ->  ( A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( cod SetCat `  U
) `  f )  =  a  ->  ( ( ( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f )  /\  A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  f )  =  a  ->  ( f ( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) )
13527, 28iscatOLD 25754 . . . 4  |-  ( ( ( ( dom SetCat `  U
)  e.  _V  /\  ( cod SetCat `  U )  e.  _V  /\  ( Id SetCat `
 U )  e. 
_V )  /\  ( ro SetCat `  U )  e.  _V )  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Cat OLD  <->  (
( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) A. h  e.  dom  ( dom SetCat `
 U ) ( ( ( ( dom SetCat `
 U ) `  h )  =  ( ( cod SetCat `  U
) `  g )  /\  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) )  /\  ( A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( cod SetCat `  U
) `  f )  =  a  ->  ( ( ( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f )  /\  A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  f )  =  a  ->  ( f ( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) ) ) )
13626, 135mp1i 11 . . 3  |-  ( U  e.  Univ  ->  ( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Cat OLD  <->  (
( <. <. ( dom SetCat `  U
) ,  ( cod SetCat `
 U ) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Ded  /\  A. f  e.  dom  ( dom
SetCat `  U ) A. g  e.  dom  ( dom SetCat `
 U ) A. h  e.  dom  ( dom SetCat `
 U ) ( ( ( ( dom SetCat `
 U ) `  h )  =  ( ( cod SetCat `  U
) `  g )  /\  ( ( dom SetCat `  U
) `  g )  =  ( ( cod SetCat `
 U ) `  f ) )  -> 
( h ( ro SetCat `
 U ) ( g ( ro SetCat `  U ) f ) )  =  ( ( h ( ro SetCat `  U ) g ) ( ro SetCat `  U
) f ) ) )  /\  ( A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( cod SetCat `  U
) `  f )  =  a  ->  ( ( ( Id SetCat `  U
) `  a )
( ro SetCat `  U
) f )  =  f )  /\  A. a  e.  dom  ( Id SetCat `
 U ) A. f  e.  dom  ( dom SetCat `
 U ) ( ( ( dom SetCat `  U
) `  f )  =  a  ->  ( f ( ro SetCat `  U
) ( ( Id SetCat `
 U ) `  a ) )  =  f ) ) ) ) )
137105, 134, 136mpbir2and 888 . 2  |-  ( U  e.  Univ  ->  <. <. ( dom
SetCat `  U ) ,  ( cod SetCat `  U
) >. ,  <. ( Id SetCat `  U ) ,  ( ro SetCat `  U ) >. >.  e.  Cat OLD  )
1381, 137eqeltrd 2357 1  |-  ( U  e.  Univ  ->  ( SetCat OLD `  U )  e.  Cat OLD  )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788    C_ wss 3152   <.cop 3643    X. cxp 4687   dom cdm 4689   ran crn 4690   Fun wfun 5249   -->wf 5251   ` cfv 5255  (class class class)co 5858   Univcgru 8412    Alg calg 25711   Dedcded 25734    Cat OLD ccatOLD 25752   Morphism SetCatccmrcase 25910   dom
SetCatcdomcase 25919   cod
SetCatccodcase 25932   Id SetCatcidcase 25939   ro SetCatcrocase 25955   SetCat OLDccaset 25976
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-map 6774  df-alg 25716  df-ded 25735  df-catOLD 25753  df-morcatset 25911  df-domcatset 25920  df-graphcatset 25922  df-codcatset 25933  df-idcatset 25940  df-rocatset 25956  df-catset 25977
  Copyright terms: Public domain W3C validator