moni

Description: Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	ismon.b	$⊢ B = {Base}_{C}$
	ismon.h	$⊢ H = Hom (C)$
	ismon.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	ismon.s	$⊢ M = Mono (C)$
	ismon.c	$⊢ φ \to C \in Cat$
	ismon.x	$⊢ φ \to X \in B$
	ismon.y	$⊢ φ \to Y \in B$
	moni.z	$⊢ φ \to Z \in B$
	moni.f	$⊢ φ \to F \in (X M Y)$
	moni.g	$⊢ φ \to G \in (Z H X)$
	moni.k	$⊢ φ \to K \in (Z H X)$
Assertion	moni	$⊢ φ \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \leftrightarrow G = K)$

Proof

Step	Hyp	Ref	Expression
1		ismon.b	$⊢ B = {Base}_{C}$
2		ismon.h	$⊢ H = Hom (C)$
3		ismon.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		ismon.s	$⊢ M = Mono (C)$
5		ismon.c	$⊢ φ \to C \in Cat$
6		ismon.x	$⊢ φ \to X \in B$
7		ismon.y	$⊢ φ \to Y \in B$
8		moni.z	$⊢ φ \to Z \in B$
9		moni.f	$⊢ φ \to F \in (X M Y)$
10		moni.g	$⊢ φ \to G \in (Z H X)$
11		moni.k	$⊢ φ \to K \in (Z H X)$
12	1 2 3 4 5 6 7	ismon2	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h)))$
13	9 12	mpbid	$⊢ φ \to (F \in (X H Y) \land \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
14	13	simprd	$⊢ φ \to \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h)$
15	10	adantr	$⊢ (φ \land z = Z) \to G \in (Z H X)$
16		simpr	$⊢ (φ \land z = Z) \to z = Z$
17	16	oveq1d	$⊢ (φ \land z = Z) \to z H X = Z H X$
18	15 17	eleqtrrd	$⊢ (φ \land z = Z) \to G \in (z H X)$
19	11	adantr	$⊢ (φ \land z = Z) \to K \in (Z H X)$
20	19 17	eleqtrrd	$⊢ (φ \land z = Z) \to K \in (z H X)$
21	20	adantr	$⊢ ((φ \land z = Z) \land g = G) \to K \in (z H X)$
22		simpllr	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to z = Z$
23	22	opeq1d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to ⟨z, X⟩ = ⟨Z, X⟩$
24	23	oveq1d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to ⟨z, X⟩ \underset{˙}{\cdot} Y = ⟨Z, X⟩ \underset{˙}{\cdot} Y$
25		eqidd	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to F = F$
26		simplr	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to g = G$
27	24 25 26	oveq123d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G$
28		simpr	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to h = K$
29	24 25 28	oveq123d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to F (⟨z, X⟩ \underset{˙}{\cdot} Y) h = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K$
30	27 29	eqeq12d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \leftrightarrow F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K)$
31	26 28	eqeq12d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to (g = h \leftrightarrow G = K)$
32	30 31	imbi12d	$⊢ (((φ \land z = Z) \land g = G) \land h = K) \to ((F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h) \leftrightarrow (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \to G = K))$
33	21 32	rspcdv	$⊢ ((φ \land z = Z) \land g = G) \to (\forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h) \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \to G = K))$
34	18 33	rspcimdv	$⊢ (φ \land z = Z) \to (\forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h) \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \to G = K))$
35	8 34	rspcimdv	$⊢ φ \to (\forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h) \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \to G = K))$
36	14 35	mpd	$⊢ φ \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \to G = K)$
37		oveq2	$⊢ G = K \to F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K$
38	36 37	impbid1	$⊢ φ \to (F (⟨Z, X⟩ \underset{˙}{\cdot} Y) G = F (⟨Z, X⟩ \underset{˙}{\cdot} Y) K \leftrightarrow G = K)$

Metamath Proof Explorer

Theorem moni

Proof