mndtccatid

	Ref	Expression
Hypotheses	mndtccat.c	No typesetting found for \|- ( ph -> C = ( MndToCat ` M ) ) with typecode \|-
	mndtccat.m	$⊢ φ \to M \in Mnd$
Assertion	mndtccatid	$⊢ φ \to (C \in Cat \land Id (C) = (y \in {Base}_{C} ⟼ 0_{M}))$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for \|- ( ph -> C = ( MndToCat ` M ) ) with typecode \|-
2		mndtccat.m	$⊢ φ \to M \in Mnd$
3		eqidd	$⊢ φ \to {Base}_{C} = {Base}_{C}$
4		eqidd	$⊢ φ \to Hom (C) = Hom (C)$
5		eqidd	$⊢ φ \to comp (C) = comp (C)$
6		fvexd	Could not format ( ph -> ( MndToCat ` M ) e. _V ) : No typesetting found for \|- ( ph -> ( MndToCat ` M ) e. _V ) with typecode \|-
7	1 6	eqeltrd	$⊢ φ \to C \in V$
8		biid	$⊢ ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w))) \leftrightarrow ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))$
9		eqid	$⊢ {Base}_{M} = {Base}_{M}$
10		eqid	$⊢ 0_{M} = 0_{M}$
11	9 10	mndidcl	$⊢ M \in Mnd \to 0_{M} \in {Base}_{M}$
12	2 11	syl	$⊢ φ \to 0_{M} \in {Base}_{M}$
13	12	adantr	$⊢ (φ \land y \in {Base}_{C}) \to 0_{M} \in {Base}_{M}$
14	1	adantr	Could not format ( ( ph /\ y e. ( Base ` C ) ) -> C = ( MndToCat ` M ) ) : No typesetting found for \|- ( ( ph /\ y e. ( Base ` C ) ) -> C = ( MndToCat ` M ) ) with typecode \|-
15	2	adantr	$⊢ (φ \land y \in {Base}_{C}) \to M \in Mnd$
16		eqidd	$⊢ (φ \land y \in {Base}_{C}) \to {Base}_{C} = {Base}_{C}$
17		simpr	$⊢ (φ \land y \in {Base}_{C}) \to y \in {Base}_{C}$
18		eqidd	$⊢ (φ \land y \in {Base}_{C}) \to Hom (C) = Hom (C)$
19	14 15 16 17 17 18	mndtchom	$⊢ (φ \land y \in {Base}_{C}) \to y Hom (C) y = {Base}_{M}$
20	13 19	eleqtrrd	$⊢ (φ \land y \in {Base}_{C}) \to 0_{M} \in (y Hom (C) y)$
21	1	adantr	Could not format ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> C = ( MndToCat ` M ) ) : No typesetting found for \|- ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> C = ( MndToCat ` M ) ) with typecode \|-
22	2	adantr	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to M \in Mnd$
23		eqidd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to {Base}_{C} = {Base}_{C}$
24		simpr1l	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to x \in {Base}_{C}$
25		simpr1r	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to y \in {Base}_{C}$
26		eqidd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to comp (C) = comp (C)$
27	21 22 23 24 25 25 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨x, y⟩ comp (C) y = +_{M}$
28	27	oveqd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to 0_{M} (⟨x, y⟩ comp (C) y) f = 0_{M} +_{M} f$
29		simpr31	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to f \in (x Hom (C) y)$
30		eqidd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to Hom (C) = Hom (C)$
31	21 22 23 24 25 30	mndtchom	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to x Hom (C) y = {Base}_{M}$
32	29 31	eleqtrd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to f \in {Base}_{M}$
33		eqid	$⊢ +_{M} = +_{M}$
34	9 33 10	mndlid	$⊢ (M \in Mnd \land f \in {Base}_{M}) \to 0_{M} +_{M} f = f$
35	22 32 34	syl2anc	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to 0_{M} +_{M} f = f$
36	28 35	eqtrd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to 0_{M} (⟨x, y⟩ comp (C) y) f = f$
37		simpr2l	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to z \in {Base}_{C}$
38	21 22 23 25 25 37 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨y, y⟩ comp (C) z = +_{M}$
39	38	oveqd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g (⟨y, y⟩ comp (C) z) 0_{M} = g +_{M} 0_{M}$
40		simpr32	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g \in (y Hom (C) z)$
41	21 22 23 25 37 30	mndtchom	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to y Hom (C) z = {Base}_{M}$
42	40 41	eleqtrd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g \in {Base}_{M}$
43	9 33 10	mndrid	$⊢ (M \in Mnd \land g \in {Base}_{M}) \to g +_{M} 0_{M} = g$
44	22 42 43	syl2anc	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g +_{M} 0_{M} = g$
45	39 44	eqtrd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g (⟨y, y⟩ comp (C) z) 0_{M} = g$
46	9 33	mndcl	$⊢ (M \in Mnd \land g \in {Base}_{M} \land f \in {Base}_{M}) \to g +_{M} f \in {Base}_{M}$
47	22 42 32 46	syl3anc	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g +_{M} f \in {Base}_{M}$
48	21 22 23 24 25 37 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨x, y⟩ comp (C) z = +_{M}$
49	48	oveqd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g (⟨x, y⟩ comp (C) z) f = g +_{M} f$
50	21 22 23 24 37 30	mndtchom	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to x Hom (C) z = {Base}_{M}$
51	47 49 50	3eltr4d	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)$
52		simpr33	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to k \in (z Hom (C) w)$
53		simpr2r	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to w \in {Base}_{C}$
54	21 22 23 37 53 30	mndtchom	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to z Hom (C) w = {Base}_{M}$
55	52 54	eleqtrd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to k \in {Base}_{M}$
56	9 33	mndass	$⊢ (M \in Mnd \land (k \in {Base}_{M} \land g \in {Base}_{M} \land f \in {Base}_{M})) \to (k +_{M} g) +_{M} f = k +_{M} (g +_{M} f)$
57	22 55 42 32 56	syl13anc	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to (k +_{M} g) +_{M} f = k +_{M} (g +_{M} f)$
58	21 22 23 24 25 53 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨x, y⟩ comp (C) w = +_{M}$
59	21 22 23 25 37 53 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨y, z⟩ comp (C) w = +_{M}$
60	59	oveqd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to k (⟨y, z⟩ comp (C) w) g = k +_{M} g$
61		eqidd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to f = f$
62	58 60 61	oveq123d	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = (k +_{M} g) +_{M} f$
63	21 22 23 24 37 53 26	mndtcco	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to ⟨x, z⟩ comp (C) w = +_{M}$
64		eqidd	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to k = k$
65	63 64 49	oveq123d	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f) = k +_{M} (g +_{M} f)$
66	57 62 65	3eqtr4d	$⊢ (φ \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z) \land k \in (z Hom (C) w)))) \to (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)$
67	3 4 5 7 8 20 36 45 51 66	iscatd2	$⊢ φ \to (C \in Cat \land Id (C) = (y \in {Base}_{C} ⟼ 0_{M}))$

Metamath Proof Explorer

Theorem mndtccatid

Proof