Metamath Proof Explorer

Theorem isepi

Description: Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b ⊢B=BaseC
isepi.h ⊢H=Hom⁡C
isepi.o ⊢·˙=comp⁡C
isepi.e ⊢E=Epi⁡C
isepi.c ⊢φ→C∈Cat
isepi.x ⊢φ→X∈B
isepi.y ⊢φ→Y∈B
Assertion isepi ⊢φ→F∈XEY↔F∈XHY∧∀z∈BFun⁡g∈YHz⟼gXY·˙zF-1

Proof

Step Hyp Ref Expression
1 isepi.b ⊢B=BaseC
2 isepi.h ⊢H=Hom⁡C
3 isepi.o ⊢·˙=comp⁡C
4 isepi.e ⊢E=Epi⁡C
5 isepi.c ⊢φ→C∈Cat
6 isepi.x ⊢φ→X∈B
7 isepi.y ⊢φ→Y∈B
8 eqid ⊢oppCat⁡C=oppCat⁡C
9 8 1 oppcbas ⊢B=BaseoppCat⁡C
10 eqid ⊢Hom⁡oppCat⁡C=Hom⁡oppCat⁡C
11 eqid ⊢comp⁡oppCat⁡C=comp⁡oppCat⁡C
12 eqid ⊢Mono⁡oppCat⁡C=Mono⁡oppCat⁡C
13 8 oppccat ⊢C∈Cat→oppCat⁡C∈Cat
14 5 13 syl ⊢φ→oppCat⁡C∈Cat
15 9 10 11 12 14 7 6 ismon ⊢φ→F∈YMono⁡oppCat⁡CX↔F∈YHom⁡oppCat⁡CX∧∀z∈BFun⁡g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg-1
16 8 5 12 4 oppcmon ⊢φ→YMono⁡oppCat⁡CX=XEY
17 16 eleq2d ⊢φ→F∈YMono⁡oppCat⁡CX↔F∈XEY
18 2 8 oppchom ⊢YHom⁡oppCat⁡CX=XHY
19 18 a1i ⊢φ→YHom⁡oppCat⁡CX=XHY
20 19 eleq2d ⊢φ→F∈YHom⁡oppCat⁡CX↔F∈XHY
21 2 8 oppchom ⊢zHom⁡oppCat⁡CY=YHz
22 21 a1i ⊢φ∧z∈B→zHom⁡oppCat⁡CY=YHz
23 simpr ⊢φ∧z∈B→z∈B
24 7 adantr ⊢φ∧z∈B→Y∈B
25 6 adantr ⊢φ∧z∈B→X∈B
26 1 3 8 23 24 25 oppcco ⊢φ∧z∈B→FzYcomp⁡oppCat⁡CXg=gXY·˙zF
27 22 26 mpteq12dv ⊢φ∧z∈B→g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg=g∈YHz⟼gXY·˙zF
28 27 cnveqd ⊢φ∧z∈B→g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg-1=g∈YHz⟼gXY·˙zF-1
29 28 funeqd ⊢φ∧z∈B→Fun⁡g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg-1↔Fun⁡g∈YHz⟼gXY·˙zF-1
30 29 ralbidva ⊢φ→∀z∈BFun⁡g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg-1↔∀z∈BFun⁡g∈YHz⟼gXY·˙zF-1
31 20 30 anbi12d ⊢φ→F∈YHom⁡oppCat⁡CX∧∀z∈BFun⁡g∈zHom⁡oppCat⁡CY⟼FzYcomp⁡oppCat⁡CXg-1↔F∈XHY∧∀z∈BFun⁡g∈YHz⟼gXY·˙zF-1
32 15 17 31 3bitr3d ⊢φ→F∈XEY↔F∈XHY∧∀z∈BFun⁡g∈YHz⟼gXY·˙zF-1