Metamath Proof Explorer


Theorem monfval

Description: Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses ismon.b B = Base C
ismon.h H = Hom C
ismon.o · ˙ = comp C
ismon.s M = Mono C
ismon.c φ C Cat
Assertion monfval φ M = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1

Proof

Step Hyp Ref Expression
1 ismon.b B = Base C
2 ismon.h H = Hom C
3 ismon.o · ˙ = comp C
4 ismon.s M = Mono C
5 ismon.c φ C Cat
6 fvexd c = C Base c V
7 fveq2 c = C Base c = Base C
8 7 1 eqtr4di c = C Base c = B
9 fvexd c = C b = B Hom c V
10 simpl c = C b = B c = C
11 10 fveq2d c = C b = B Hom c = Hom C
12 11 2 eqtr4di c = C b = B Hom c = H
13 simplr c = C b = B h = H b = B
14 simpr c = C b = B h = H h = H
15 14 oveqd c = C b = B h = H x h y = x H y
16 14 oveqd c = C b = B h = H z h x = z H x
17 simpll c = C b = B h = H c = C
18 17 fveq2d c = C b = B h = H comp c = comp C
19 18 3 eqtr4di c = C b = B h = H comp c = · ˙
20 19 oveqd c = C b = B h = H z x comp c y = z x · ˙ y
21 20 oveqd c = C b = B h = H f z x comp c y g = f z x · ˙ y g
22 16 21 mpteq12dv c = C b = B h = H g z h x f z x comp c y g = g z H x f z x · ˙ y g
23 22 cnveqd c = C b = B h = H g z h x f z x comp c y g -1 = g z H x f z x · ˙ y g -1
24 23 funeqd c = C b = B h = H Fun g z h x f z x comp c y g -1 Fun g z H x f z x · ˙ y g -1
25 13 24 raleqbidv c = C b = B h = H z b Fun g z h x f z x comp c y g -1 z B Fun g z H x f z x · ˙ y g -1
26 15 25 rabeqbidv c = C b = B h = H f x h y | z b Fun g z h x f z x comp c y g -1 = f x H y | z B Fun g z H x f z x · ˙ y g -1
27 13 13 26 mpoeq123dv c = C b = B h = H x b , y b f x h y | z b Fun g z h x f z x comp c y g -1 = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1
28 9 12 27 csbied2 c = C b = B Hom c / h x b , y b f x h y | z b Fun g z h x f z x comp c y g -1 = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1
29 6 8 28 csbied2 c = C Base c / b Hom c / h x b , y b f x h y | z b Fun g z h x f z x comp c y g -1 = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1
30 df-mon Mono = c Cat Base c / b Hom c / h x b , y b f x h y | z b Fun g z h x f z x comp c y g -1
31 1 fvexi B V
32 31 31 mpoex x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1 V
33 29 30 32 fvmpt C Cat Mono C = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1
34 5 33 syl φ Mono C = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1
35 4 34 eqtrid φ M = x B , y B f x H y | z B Fun g z H x f z x · ˙ y g -1