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

Definition df-epi 16612
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 16610 . 2 class Epi
2 vc . . 3 setvar 𝑐
3 ccat 16546 . . 3 class Cat
42cv 1631 . . . . . 6 class 𝑐
5 coppc 16592 . . . . . 6 class oppCat
64, 5cfv 6049 . . . . 5 class (oppCat‘𝑐)
7 cmon 16609 . . . . 5 class Mono
86, 7cfv 6049 . . . 4 class (Mono‘(oppCat‘𝑐))
98ctpos 7521 . . 3 class tpos (Mono‘(oppCat‘𝑐))
102, 3, 9cmpt 4881 . 2 class (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
111, 10wceq 1632 1 wff Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  oppcmon  16619
  Copyright terms: Public domain W3C validator