Metamath Proof Explorer

Theorem monhom

Description: A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-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
ismon.x ⊢ φ → X ∈ B
ismon.y ⊢ φ → Y ∈ B
Assertion monhom ⊢ φ → X M Y ⊆ X H Y

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 ismon.x ⊢ φ → X ∈ B
7 ismon.y ⊢ φ → Y ∈ B
8 1 2 3 4 5 6 7 ismon ⊢ φ → f ∈ X M Y ↔ f ∈ X H Y ∧ ∀ z ∈ B Fun ⁡ g ∈ z H X ⟼ f z X · ˙ Y g -1
9 simpl ⊢ f ∈ X H Y ∧ ∀ z ∈ B Fun ⁡ g ∈ z H X ⟼ f z X · ˙ Y g -1 → f ∈ X H Y
10 8 9 biimtrdi ⊢ φ → f ∈ X M Y → f ∈ X H Y
11 10 ssrdv ⊢ φ → X M Y ⊆ X H Y