This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC CATEGORY THEORY Categories Monomorphisms and epimorphisms df-epi
Description: Function returning the epimorphisms of the category c . JFM CAT_1
def. 11. (Contributed by FL , 8-Aug-2008) (Revised by Mario Carneiro , 2-Jan-2017)
Ref
Expression
Assertion
df-epi ⊢ Epi = ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cepi ⊢ Epi
1
vc ⊢ 𝑐
2
ccat ⊢ Cat
3
cmon ⊢ Mono
4
coppc ⊢ oppCat
5
1
cv ⊢ 𝑐
6
5 4
cfv ⊢ ( oppCat ‘ 𝑐 )
7
6 3
cfv ⊢ ( Mono ‘ ( oppCat ‘ 𝑐 ) )
8
7
ctpos ⊢ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) )
9
1 2 8
cmpt ⊢ ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )
10
0 9
wceq ⊢ Epi = ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )