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 16595
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 16593 . 2 class Epi
2 vc . . 3 setvar 𝑐
3 ccat 16529 . . 3 class Cat
42cv 1636 . . . . . 6 class 𝑐
5 coppc 16575 . . . . . 6 class oppCat
64, 5cfv 6101 . . . . 5 class (oppCat‘𝑐)
7 cmon 16592 . . . . 5 class Mono
86, 7cfv 6101 . . . 4 class (Mono‘(oppCat‘𝑐))
98ctpos 7586 . . 3 class tpos (Mono‘(oppCat‘𝑐))
102, 3, 9cmpt 4923 . 2 class (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
111, 10wceq 1637 1 wff Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  oppcmon  16602
  Copyright terms: Public domain W3C validator