Metamath Proof Explorer

Theorem epihom

Description: An epimorphism is a morphism. (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 epihom ⊢ φ → X E Y ⊆ X H Y

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 simpl ⊢ f ∈ X H Y ∧ ∀ z ∈ B Fun ⁡ g ∈ Y H z ⟼ g X Y · ˙ z f -1 → f ∈ X H Y
10 8 9 syl6bi ⊢ φ → f ∈ X E Y → f ∈ X H Y
11 10 ssrdv ⊢ φ → X E Y ⊆ X H Y