Theorem epii

Description: Property of an epimorphism. (Contributed by Mario Carneiro, 3-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$$
	epii.z	$$⊢\phi \to Z\in B$$
	epii.f	$$⊢\phi \to F\in \left(XEY\right)$$
	epii.g	$$⊢\phi \to G\in \left(YHZ\right)$$
	epii.k	$$⊢\phi \to K\in \left(YHZ\right)$$
Assertion	epii	$$⊢\phi \to \left(G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=K\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\leftrightarrow G=K\right)$$

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		epii.z	$$⊢\phi \to Z\in B$$
9		epii.f	$$⊢\phi \to F\in \left(XEY\right)$$
10		epii.g	$$⊢\phi \to G\in \left(YHZ\right)$$
11		epii.k	$$⊢\phi \to K\in \left(YHZ\right)$$
12		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
13	1 3 12 8 7 6	oppcco	$$⊢\phi \to F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)G=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
14	1 3 12 8 7 6	oppcco	$$⊢\phi \to F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)K=K\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
15	13 14	eqeq12d	$$⊢\phi \to \left(F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)G=F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)K\leftrightarrow G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=K\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)$$
16	12 1	oppcbas	$$⊢B={\mathrm{Base}}_{\mathrm{oppCat}\left(C\right)}$$
17		eqid	$$⊢\mathrm{Hom}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{Hom}\left(\mathrm{oppCat}\left(C\right)\right)$$
18		eqid	$$⊢\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)$$
19		eqid	$$⊢\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)$$
20	12	oppccat	$$⊢C\in \mathrm{Cat}\to \mathrm{oppCat}\left(C\right)\in \mathrm{Cat}$$
21	5 20	syl	$$⊢\phi \to \mathrm{oppCat}\left(C\right)\in \mathrm{Cat}$$
22	12 5 19 4	oppcmon	$$⊢\phi \to Y\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)X=XEY$$
23	9 22	eleqtrrd	$$⊢\phi \to F\in \left(Y\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)X\right)$$
24	2 12	oppchom	$$⊢Z\mathrm{Hom}\left(\mathrm{oppCat}\left(C\right)\right)Y=YHZ$$
25	10 24	eleqtrrdi	$$⊢\phi \to G\in \left(Z\mathrm{Hom}\left(\mathrm{oppCat}\left(C\right)\right)Y\right)$$
26	11 24	eleqtrrdi	$$⊢\phi \to K\in \left(Z\mathrm{Hom}\left(\mathrm{oppCat}\left(C\right)\right)Y\right)$$
27	16 17 18 19 21 7 6 8 23 25 26	moni	$$⊢\phi \to \left(F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)G=F\left(⟨Z,Y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(C\right)\right)X\right)K\leftrightarrow G=K\right)$$
28	15 27	bitr3d	$$⊢\phi \to \left(G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=K\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\leftrightarrow G=K\right)$$