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

Definition df-isoc 25808
 Description: Function returning the isomorphisms of the category . The Joy of Cats p. 28. (Contributed by FL, 9-Jun-2014.)
Assertion
Ref Expression
df-isoc
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-isoc
StepHypRef Expression
1 cisoOLD 25805 . 2
2 vx . . 3
3 ccatOLD 25752 . . 3
4 vg . . . . . . . . 9
54cv 1622 . . . . . . . 8
62cv 1622 . . . . . . . . 9
7 cdom_ 25712 . . . . . . . . 9
86, 7cfv 5255 . . . . . . . 8
95, 8cfv 5255 . . . . . . 7
10 vf . . . . . . . . 9
1110cv 1622 . . . . . . . 8
12 ccod_ 25713 . . . . . . . . 9
136, 12cfv 5255 . . . . . . . 8
1411, 13cfv 5255 . . . . . . 7
159, 14wceq 1623 . . . . . 6
165, 13cfv 5255 . . . . . . 7
1711, 8cfv 5255 . . . . . . 7
1816, 17wceq 1623 . . . . . 6
19 co_ 25715 . . . . . . . . . 10
206, 19cfv 5255 . . . . . . . . 9
2111, 5, 20co 5858 . . . . . . . 8
22 cid_ 25714 . . . . . . . . . 10
236, 22cfv 5255 . . . . . . . . 9
249, 23cfv 5255 . . . . . . . 8
2521, 24wceq 1623 . . . . . . 7
265, 11, 20co 5858 . . . . . . . 8
2717, 23cfv 5255 . . . . . . . 8
2826, 27wceq 1623 . . . . . . 7
2925, 28wa 358 . . . . . 6
3015, 18, 29w3a 934 . . . . 5
318cdm 4689 . . . . 5
3230, 4, 31wrex 2544 . . . 4
3332, 10, 31crab 2547 . . 3
342, 3, 33cmpt 4077 . 2
351, 34wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  isiso  25825
 Copyright terms: Public domain W3C validator