Metamath Proof Explorer


Theorem isepi2

Description: Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b B = Base C
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 isepi2 φ F X E Y F X H Y z B g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h

Proof

Step Hyp Ref Expression
1 isepi.b B = Base C
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 1 2 3 4 5 6 7 isepi φ F X E Y F X H Y z B Fun g Y H z g X Y · ˙ z F -1
9 5 ad2antrr φ F X H Y z B g Y H z C Cat
10 6 ad2antrr φ F X H Y z B g Y H z X B
11 7 ad2antrr φ F X H Y z B g Y H z Y B
12 simprl φ F X H Y z B g Y H z z B
13 simplr φ F X H Y z B g Y H z F X H Y
14 simprr φ F X H Y z B g Y H z g Y H z
15 1 2 3 9 10 11 12 13 14 catcocl φ F X H Y z B g Y H z g X Y · ˙ z F X H z
16 15 anassrs φ F X H Y z B g Y H z g X Y · ˙ z F X H z
17 16 ralrimiva φ F X H Y z B g Y H z g X Y · ˙ z F X H z
18 eqid g Y H z g X Y · ˙ z F = g Y H z g X Y · ˙ z F
19 18 fmpt g Y H z g X Y · ˙ z F X H z g Y H z g X Y · ˙ z F : Y H z X H z
20 df-f1 g Y H z g X Y · ˙ z F : Y H z 1-1 X H z g Y H z g X Y · ˙ z F : Y H z X H z Fun g Y H z g X Y · ˙ z F -1
21 20 baib g Y H z g X Y · ˙ z F : Y H z X H z g Y H z g X Y · ˙ z F : Y H z 1-1 X H z Fun g Y H z g X Y · ˙ z F -1
22 19 21 sylbi g Y H z g X Y · ˙ z F X H z g Y H z g X Y · ˙ z F : Y H z 1-1 X H z Fun g Y H z g X Y · ˙ z F -1
23 oveq1 g = h g X Y · ˙ z F = h X Y · ˙ z F
24 18 23 f1mpt g Y H z g X Y · ˙ z F : Y H z 1-1 X H z g Y H z g X Y · ˙ z F X H z g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
25 24 baib g Y H z g X Y · ˙ z F X H z g Y H z g X Y · ˙ z F : Y H z 1-1 X H z g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
26 22 25 bitr3d g Y H z g X Y · ˙ z F X H z Fun g Y H z g X Y · ˙ z F -1 g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
27 17 26 syl φ F X H Y z B Fun g Y H z g X Y · ˙ z F -1 g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
28 27 ralbidva φ F X H Y z B Fun g Y H z g X Y · ˙ z F -1 z B g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
29 28 pm5.32da φ F X H Y z B Fun g Y H z g X Y · ˙ z F -1 F X H Y z B g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h
30 8 29 bitrd φ F X E Y F X H Y z B g Y H z h Y H z g X Y · ˙ z F = h X Y · ˙ z F g = h