Metamath Proof Explorer

Definition df-mon

Description: Function returning the monomorphisms of the category c . JFM CAT_1 def. 10. (Contributed by FL, 5-Dec-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmon class Mono
1 vc setvar c
2 ccat class Cat
3 cbs class Base
4 1 cv setvar c
5 4 3 cfv class Base c
6 vb setvar b
7 chom class Hom
8 4 7 cfv class Hom ⁡ c
9 vh setvar h
10 vx setvar x
11 6 cv setvar b
12 vy setvar y
13 vf setvar f
14 10 cv setvar x
15 9 cv setvar h
16 12 cv setvar y
17 14 16 15 co class x h y
18 vz setvar z
19 vg setvar g
20 18 cv setvar z
21 20 14 15 co class z h x
22 13 cv setvar f
23 20 14 cop class z x
24 cco class comp
25 4 24 cfv class comp ⁡ c
26 23 16 25 co class z x comp ⁡ c y
27 19 cv setvar g
28 22 27 26 co class f z x comp ⁡ c y g
29 19 21 28 cmpt class g ∈ z h x ⟼ f z x comp ⁡ c y g
30 29 ccnv class g ∈ z h x ⟼ f z x comp ⁡ c y g -1
31 30 wfun wff Fun ⁡ g ∈ z h x ⟼ f z x comp ⁡ c y g -1
32 31 18 11 wral wff ∀ z ∈ b Fun ⁡ g ∈ z h x ⟼ f z x comp ⁡ c y g -1
33 32 13 17 crab class f ∈ x h y | ∀ z ∈ b Fun ⁡ g ∈ z h x ⟼ f z x comp ⁡ c y g -1
34 10 12 11 11 33 cmpo class x ∈ b , y ∈ b ⟼ f ∈ x h y | ∀ z ∈ b Fun ⁡ g ∈ z h x ⟼ f z x comp ⁡ c y g -1
35 9 8 34 csb class ⦋ 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
36 6 5 35 csb class ⦋ 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
37 1 2 36 cmpt class 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
38 0 37 wceq wff 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