mndtccatid - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mndtccatid		Structured version Visualization version GIF version

Theorem mndtccatid 47666

Description: Lemma for mndtccat 47667 and mndtcid 47668. (Contributed by Zhi Wang, 22-Sep-2024.)

**Hypotheses**
Ref	Expression
mndtccat.c	⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))
mndtccat.m	⊢ (𝜑 → 𝑀 ∈ Mnd)

**Assertion**
Ref	Expression
mndtccatid	⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0_g‘𝑀))))

Distinct variable groups: 𝑦,𝐶 𝜑,𝑦 Allowed substitution hint: 𝑀(𝑦)

Proof of Theorem mndtccatid Dummy variables 𝑓 𝑔 𝑘 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2733	. 2 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐶))
2		eqidd 2733	. 2 ⊢ (𝜑 → (Hom ‘𝐶) = (Hom ‘𝐶))
3		eqidd 2733	. 2 ⊢ (𝜑 → (comp‘𝐶) = (comp‘𝐶))
4		mndtccat.c	. . 3 ⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))
5		fvexd 6903	. . 3 ⊢ (𝜑 → (MndToCat‘𝑀) ∈ V)
6	4, 5	eqeltrd 2833	. 2 ⊢ (𝜑 → 𝐶 ∈ V)
7		biid 260	. 2 ⊢ (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))) ↔ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))))
8		mndtccat.m	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ Mnd)
9		eqid 2732	. . . . . 6 ⊢ (Base‘𝑀) = (Base‘𝑀)
10		eqid 2732	. . . . . 6 ⊢ (0_g‘𝑀) = (0_g‘𝑀)
11	9, 10	mndidcl 18636	. . . . 5 ⊢ (𝑀 ∈ Mnd → (0_g‘𝑀) ∈ (Base‘𝑀))
12	8, 11	syl 17	. . . 4 ⊢ (𝜑 → (0_g‘𝑀) ∈ (Base‘𝑀))
13	12	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → (0_g‘𝑀) ∈ (Base‘𝑀))
14	4	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐶 = (MndToCat‘𝑀))
15	8	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑀 ∈ Mnd)
16		eqidd 2733	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐶))
17		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
18		eqidd 2733	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → (Hom ‘𝐶) = (Hom ‘𝐶))
19	14, 15, 16, 17, 17, 18	mndtchom 47663	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑦) = (Base‘𝑀))
20	13, 19	eleqtrrd 2836	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → (0_g‘𝑀) ∈ (𝑦(Hom ‘𝐶)𝑦))
21	4	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝐶 = (MndToCat‘𝑀))
22	8	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑀 ∈ Mnd)
23		eqidd 2733	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (Base‘𝐶) = (Base‘𝐶))
24		simpr1l 1230	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑥 ∈ (Base‘𝐶))
25		simpr1r 1231	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑦 ∈ (Base‘𝐶))
26		eqidd 2733	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (comp‘𝐶) = (comp‘𝐶))
27	21, 22, 23, 24, 25, 25, 26	mndtcco 47664	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑦) = (+_g‘𝑀))
28	27	oveqd 7422	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((0_g‘𝑀)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑦)𝑓) = ((0_g‘𝑀)(+_g‘𝑀)𝑓))
29		simpr31 1263	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
30		eqidd 2733	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (Hom ‘𝐶) = (Hom ‘𝐶))
31	21, 22, 23, 24, 25, 30	mndtchom 47663	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑥(Hom ‘𝐶)𝑦) = (Base‘𝑀))
32	29, 31	eleqtrd 2835	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑓 ∈ (Base‘𝑀))
33		eqid 2732	. . . . 5 ⊢ (+_g‘𝑀) = (+_g‘𝑀)
34	9, 33, 10	mndlid 18641	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ (Base‘𝑀)) → ((0_g‘𝑀)(+_g‘𝑀)𝑓) = 𝑓)
35	22, 32, 34	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((0_g‘𝑀)(+_g‘𝑀)𝑓) = 𝑓)
36	28, 35	eqtrd 2772	. 2 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((0_g‘𝑀)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑦)𝑓) = 𝑓)
37		simpr2l 1232	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑧 ∈ (Base‘𝐶))
38	21, 22, 23, 25, 25, 37, 26	mndtcco 47664	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑦, 𝑦⟩(comp‘𝐶)𝑧) = (+_g‘𝑀))
39	38	oveqd 7422	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(⟨𝑦, 𝑦⟩(comp‘𝐶)𝑧)(0_g‘𝑀)) = (𝑔(+_g‘𝑀)(0_g‘𝑀)))
40		simpr32 1264	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
41	21, 22, 23, 25, 37, 30	mndtchom 47663	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑦(Hom ‘𝐶)𝑧) = (Base‘𝑀))
42	40, 41	eleqtrd 2835	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑔 ∈ (Base‘𝑀))
43	9, 33, 10	mndrid 18642	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝑔 ∈ (Base‘𝑀)) → (𝑔(+_g‘𝑀)(0_g‘𝑀)) = 𝑔)
44	22, 42, 43	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(+_g‘𝑀)(0_g‘𝑀)) = 𝑔)
45	39, 44	eqtrd 2772	. 2 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(⟨𝑦, 𝑦⟩(comp‘𝐶)𝑧)(0_g‘𝑀)) = 𝑔)
46	9, 33	mndcl 18629	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝑔 ∈ (Base‘𝑀) ∧ 𝑓 ∈ (Base‘𝑀)) → (𝑔(+_g‘𝑀)𝑓) ∈ (Base‘𝑀))
47	22, 42, 32, 46	syl3anc 1371	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(+_g‘𝑀)𝑓) ∈ (Base‘𝑀))
48	21, 22, 23, 24, 25, 37, 26	mndtcco 47664	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧) = (+_g‘𝑀))
49	48	oveqd 7422	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(+_g‘𝑀)𝑓))
50	21, 22, 23, 24, 37, 30	mndtchom 47663	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑥(Hom ‘𝐶)𝑧) = (Base‘𝑀))
51	47, 49, 50	3eltr4d 2848	. 2 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
52		simpr33 1265	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
53		simpr2r 1233	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑤 ∈ (Base‘𝐶))
54	21, 22, 23, 37, 53, 30	mndtchom 47663	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑧(Hom ‘𝐶)𝑤) = (Base‘𝑀))
55	52, 54	eleqtrd 2835	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑘 ∈ (Base‘𝑀))
56	9, 33	mndass 18630	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ (𝑘 ∈ (Base‘𝑀) ∧ 𝑔 ∈ (Base‘𝑀) ∧ 𝑓 ∈ (Base‘𝑀))) → ((𝑘(+_g‘𝑀)𝑔)(+_g‘𝑀)𝑓) = (𝑘(+_g‘𝑀)(𝑔(+_g‘𝑀)𝑓)))
57	22, 55, 42, 32, 56	syl13anc 1372	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((𝑘(+_g‘𝑀)𝑔)(+_g‘𝑀)𝑓) = (𝑘(+_g‘𝑀)(𝑔(+_g‘𝑀)𝑓)))
58	21, 22, 23, 24, 25, 53, 26	mndtcco 47664	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤) = (+_g‘𝑀))
59	21, 22, 23, 25, 37, 53, 26	mndtcco 47664	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤) = (+_g‘𝑀))
60	59	oveqd 7422	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (𝑘(+_g‘𝑀)𝑔))
61		eqidd 2733	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑓 = 𝑓)
62	58, 60, 61	oveq123d 7426	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((𝑘(+_g‘𝑀)𝑔)(+_g‘𝑀)𝑓))
63	21, 22, 23, 24, 37, 53, 26	mndtcco 47664	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤) = (+_g‘𝑀))
64		eqidd 2733	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → 𝑘 = 𝑘)
65	63, 64, 49	oveq123d 7426	. . 3 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (𝑘(+_g‘𝑀)(𝑔(+_g‘𝑀)𝑓)))
66	57, 62, 65	3eqtr4d 2782	. 2 ⊢ ((𝜑 ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))) → ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
67	1, 2, 3, 6, 7, 20, 36, 45, 51, 66	iscatd2 17621	1 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0_g‘𝑀))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 Vcvv 3474 ⟨cop 4633 ↦ cmpt 5230 ‘cfv 6540 (class class class)co 7405 Basecbs 17140 +_gcplusg 17193 Hom chom 17204 compcco 17205 0_gc0g 17381 Catccat 17604 Idccid 17605 Mndcmnd 18621 MndToCatcmndtc 47656

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-ot 4636 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-struct 17076 df-slot 17111 df-ndx 17123 df-base 17141 df-hom 17217 df-cco 17218 df-0g 17383 df-cat 17608 df-cid 17609 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-mndtc 47657

This theorem is referenced by: mndtccat 47667 mndtcid 47668

W3C validator