Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-epi Structured version   Visualization version   GIF version

Definition df-epi 16214
 Description: Function returning the epimorphisms of the category 𝑐. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-epi Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))

Detailed syntax breakdown of Definition df-epi
StepHypRef Expression
1 cepi 16212 . 2 class Epi
2 vc . . 3 setvar 𝑐
3 ccat 16148 . . 3 class Cat
42cv 1474 . . . . . 6 class 𝑐
5 coppc 16194 . . . . . 6 class oppCat
64, 5cfv 5804 . . . . 5 class (oppCat‘𝑐)
7 cmon 16211 . . . . 5 class Mono
86, 7cfv 5804 . . . 4 class (Mono‘(oppCat‘𝑐))
98ctpos 7238 . . 3 class tpos (Mono‘(oppCat‘𝑐))
102, 3, 9cmpt 4643 . 2 class (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
111, 10wceq 1475 1 wff Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
 Colors of variables: wff setvar class This definition is referenced by:  oppcmon  16221
 Copyright terms: Public domain W3C validator