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

Definition df-isof 25945
Description: Class of isomorphisms. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-isof  |-  Isofunc  =  ( u  e.  Cat OLD  ,  v  e.  Cat OLD  |->  { f  e.  (
Func OLD `  <. u ,  v >. )  |  E. g  e.  (
Func OLD `  <. v ,  u >. ) ( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f )  =  (  _I  |`  dom  ( dom_ `  u ) ) ) } )
Distinct variable group:    v, u, f, g

Detailed syntax breakdown of Definition df-isof
StepHypRef Expression
1 cifunc 25935 . 2  class  Isofunc
2 vu . . 3  set  u
3 vv . . 3  set  v
4 ccatOLD 25855 . . 3  class  Cat OLD
5 vf . . . . . . . . 9  set  f
65cv 1631 . . . . . . . 8  class  f
7 vg . . . . . . . . 9  set  g
87cv 1631 . . . . . . . 8  class  g
96, 8ccom 4709 . . . . . . 7  class  ( f  o.  g )
10 cid 4320 . . . . . . . 8  class  _I
113cv 1631 . . . . . . . . . 10  class  v
12 cdom_ 25815 . . . . . . . . . 10  class  dom_
1311, 12cfv 5271 . . . . . . . . 9  class  ( dom_ `  v )
1413cdm 4705 . . . . . . . 8  class  dom  ( dom_ `  v )
1510, 14cres 4707 . . . . . . 7  class  (  _I  |`  dom  ( dom_ `  v
) )
169, 15wceq 1632 . . . . . 6  wff  ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )
178, 6ccom 4709 . . . . . . 7  class  ( g  o.  f )
182cv 1631 . . . . . . . . . 10  class  u
1918, 12cfv 5271 . . . . . . . . 9  class  ( dom_ `  u )
2019cdm 4705 . . . . . . . 8  class  dom  ( dom_ `  u )
2110, 20cres 4707 . . . . . . 7  class  (  _I  |`  dom  ( dom_ `  u
) )
2217, 21wceq 1632 . . . . . 6  wff  ( g  o.  f )  =  (  _I  |`  dom  ( dom_ `  u ) )
2316, 22wa 358 . . . . 5  wff  ( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f )  =  (  _I  |`  dom  ( dom_ `  u ) ) )
2411, 18cop 3656 . . . . . 6  class  <. v ,  u >.
25 cfuncOLD 25934 . . . . . 6  class  Func OLD
2624, 25cfv 5271 . . . . 5  class  ( Func
OLD `  <. v ,  u >. )
2723, 7, 26wrex 2557 . . . 4  wff  E. g  e.  ( Func OLD `  <. v ,  u >. )
( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f
)  =  (  _I  |`  dom  ( dom_ `  u
) ) )
2818, 11cop 3656 . . . . 5  class  <. u ,  v >.
2928, 25cfv 5271 . . . 4  class  ( Func
OLD `  <. u ,  v >. )
3027, 5, 29crab 2560 . . 3  class  { f  e.  ( Func OLD ` 
<. u ,  v >.
)  |  E. g  e.  ( Func OLD `  <. v ,  u >. )
( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f
)  =  (  _I  |`  dom  ( dom_ `  u
) ) ) }
312, 3, 4, 4, 30cmpt2 5876 . 2  class  ( u  e.  Cat OLD  , 
v  e.  Cat OLD  |->  { f  e.  (
Func OLD `  <. u ,  v >. )  |  E. g  e.  (
Func OLD `  <. v ,  u >. ) ( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f )  =  (  _I  |`  dom  ( dom_ `  u ) ) ) } )
321, 31wceq 1632 1  wff  Isofunc  =  ( u  e.  Cat OLD  ,  v  e.  Cat OLD  |->  { f  e.  (
Func OLD `  <. u ,  v >. )  |  E. g  e.  (
Func OLD `  <. v ,  u >. ) ( ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )  /\  ( g  o.  f )  =  (  _I  |`  dom  ( dom_ `  u ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator