Theorem epihom

Description: An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	isepi.b	$$⊢B={\mathrm{Base}}_C$$
	isepi.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	isepi.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	isepi.e	$$⊢E=\mathrm{Epi}\left(C\right)$$
	isepi.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	isepi.x	$$⊢\phi \to X\in B$$
	isepi.y	$$⊢\phi \to Y\in B$$
Assertion	epihom	$$⊢\phi \to XEY\subseteq XHY$$

Proof

Step	Hyp	Ref	Expression
1		isepi.b	$$⊢B={\mathrm{Base}}_C$$
2		isepi.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		isepi.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		isepi.e	$$⊢E=\mathrm{Epi}\left(C\right)$$
5		isepi.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		isepi.x	$$⊢\phi \to X\in B$$
7		isepi.y	$$⊢\phi \to Y\in B$$
8	1 2 3 4 5 6 7	isepi	$$⊢\phi \to \left(f\in \left(XEY\right)\leftrightarrow \left(f\in \left(XHY\right)\wedge \forall z\in B\mathrm{Fun}{\left(g\in \left(YHz\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}z\right)f\right)}^{-1}\right)\right)$$
9		simpl	$$⊢\left(f\in \left(XHY\right)\wedge \forall z\in B\mathrm{Fun}{\left(g\in \left(YHz\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}z\right)f\right)}^{-1}\right)\to f\in \left(XHY\right)$$
10	8 9	biimtrdi	$$⊢\phi \to \left(f\in \left(XEY\right)\to f\in \left(XHY\right)\right)$$
11	10	ssrdv	$$⊢\phi \to XEY\subseteq XHY$$