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 syl5eq ⊢ φ → M = x ∈ B , y ∈ B ⟼ f ∈ x H y | ∀ z ∈ B Fun ⁡ g ∈ z H x ⟼ f z x · ˙ y g -1