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 25842
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 25832 . 2  class  Isofunc
2 vu . . 3  set  u
3 vv . . 3  set  v
4 ccatOLD 25752 . . 3  class  Cat OLD
5 vf . . . . . . . . 9  set  f
65cv 1622 . . . . . . . 8  class  f
7 vg . . . . . . . . 9  set  g
87cv 1622 . . . . . . . 8  class  g
96, 8ccom 4693 . . . . . . 7  class  ( f  o.  g )
10 cid 4304 . . . . . . . 8  class  _I
113cv 1622 . . . . . . . . . 10  class  v
12 cdom_ 25712 . . . . . . . . . 10  class  dom_
1311, 12cfv 5255 . . . . . . . . 9  class  ( dom_ `  v )
1413cdm 4689 . . . . . . . 8  class  dom  ( dom_ `  v )
1510, 14cres 4691 . . . . . . 7  class  (  _I  |`  dom  ( dom_ `  v
) )
169, 15wceq 1623 . . . . . 6  wff  ( f  o.  g )  =  (  _I  |`  dom  ( dom_ `  v ) )
178, 6ccom 4693 . . . . . . 7  class  ( g  o.  f )
182cv 1622 . . . . . . . . . 10  class  u
1918, 12cfv 5255 . . . . . . . . 9  class  ( dom_ `  u )
2019cdm 4689 . . . . . . . 8  class  dom  ( dom_ `  u )
2110, 20cres 4691 . . . . . . 7  class  (  _I  |`  dom  ( dom_ `  u
) )
2217, 21wceq 1623 . . . . . 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 3643 . . . . . 6  class  <. v ,  u >.
25 cfuncOLD 25831 . . . . . 6  class  Func OLD
2624, 25cfv 5255 . . . . 5  class  ( Func
OLD `  <. v ,  u >. )
2723, 7, 26wrex 2544 . . . 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 3643 . . . . 5  class  <. u ,  v >.
2928, 25cfv 5255 . . . 4  class  ( Func
OLD `  <. u ,  v >. )
3027, 5, 29crab 2547 . . 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 5860 . 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 1623 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