Metamath Proof Explorer

Theorem mndtccatid

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

Ref Expression
Hypotheses mndtccat.c No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
mndtccat.m ⊢φ→M∈Mnd
Assertion mndtccatid ⊢φ→C∈Cat∧Id⁡C=y∈BaseC⟼0M

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 ⊢φ→M∈Mnd
3 eqidd ⊢φ→BaseC=BaseC
4 eqidd ⊢φ→Hom⁡C=Hom⁡C
5 eqidd ⊢φ→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 ⊢φ→C∈V
8 biid ⊢x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw↔x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw
9 eqid ⊢BaseM=BaseM
10 eqid ⊢0M=0M
11 9 10 mndidcl ⊢M∈Mnd→0M∈BaseM
12 2 11 syl ⊢φ→0M∈BaseM
13 12 adantr ⊢φ∧y∈BaseC→0M∈BaseM
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 ⊢φ∧y∈BaseC→M∈Mnd
16 eqidd ⊢φ∧y∈BaseC→BaseC=BaseC
17 simpr ⊢φ∧y∈BaseC→y∈BaseC
18 eqidd ⊢φ∧y∈BaseC→Hom⁡C=Hom⁡C
19 14 15 16 17 17 18 mndtchom ⊢φ∧y∈BaseC→yHom⁡Cy=BaseM
20 13 19 eleqtrrd ⊢φ∧y∈BaseC→0M∈yHom⁡Cy
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 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→M∈Mnd
23 eqidd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→BaseC=BaseC
24 simpr1l ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→x∈BaseC
25 simpr1r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→y∈BaseC
26 eqidd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→comp⁡C=comp⁡C
27 21 22 23 24 25 25 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xycomp⁡Cy=+M
28 27 oveqd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→0Mxycomp⁡Cyf=0M+Mf
29 simpr31 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→f∈xHom⁡Cy
30 eqidd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→Hom⁡C=Hom⁡C
31 21 22 23 24 25 30 mndtchom ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xHom⁡Cy=BaseM
32 29 31 eleqtrd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→f∈BaseM
33 eqid ⊢+M=+M
34 9 33 10 mndlid ⊢M∈Mnd∧f∈BaseM→0M+Mf=f
35 22 32 34 syl2anc ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→0M+Mf=f
36 28 35 eqtrd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→0Mxycomp⁡Cyf=f
37 simpr2l ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→z∈BaseC
38 21 22 23 25 25 37 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→yycomp⁡Cz=+M
39 38 oveqd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→gyycomp⁡Cz0M=g+M0M
40 simpr32 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→g∈yHom⁡Cz
41 21 22 23 25 37 30 mndtchom ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→yHom⁡Cz=BaseM
42 40 41 eleqtrd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→g∈BaseM
43 9 33 10 mndrid ⊢M∈Mnd∧g∈BaseM→g+M0M=g
44 22 42 43 syl2anc ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→g+M0M=g
45 39 44 eqtrd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→gyycomp⁡Cz0M=g
46 9 33 mndcl ⊢M∈Mnd∧g∈BaseM∧f∈BaseM→g+Mf∈BaseM
47 22 42 32 46 syl3anc ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→g+Mf∈BaseM
48 21 22 23 24 25 37 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xycomp⁡Cz=+M
49 48 oveqd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→gxycomp⁡Czf=g+Mf
50 21 22 23 24 37 30 mndtchom ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xHom⁡Cz=BaseM
51 47 49 50 3eltr4d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→gxycomp⁡Czf∈xHom⁡Cz
52 simpr33 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→k∈zHom⁡Cw
53 simpr2r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→w∈BaseC
54 21 22 23 37 53 30 mndtchom ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→zHom⁡Cw=BaseM
55 52 54 eleqtrd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→k∈BaseM
56 9 33 mndass ⊢M∈Mnd∧k∈BaseM∧g∈BaseM∧f∈BaseM→k+Mg+Mf=k+Mg+Mf
57 22 55 42 32 56 syl13anc ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→k+Mg+Mf=k+Mg+Mf
58 21 22 23 24 25 53 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xycomp⁡Cw=+M
59 21 22 23 25 37 53 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→yzcomp⁡Cw=+M
60 59 oveqd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→kyzcomp⁡Cwg=k+Mg
61 eqidd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→f=f
62 58 60 61 oveq123d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→kyzcomp⁡Cwgxycomp⁡Cwf=k+Mg+Mf
63 21 22 23 24 37 53 26 mndtcco ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→xzcomp⁡Cw=+M
64 eqidd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→k=k
65 63 64 49 oveq123d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→kxzcomp⁡Cwgxycomp⁡Czf=k+Mg+Mf
66 57 62 65 3eqtr4d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧w∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧k∈zHom⁡Cw→kyzcomp⁡Cwgxycomp⁡Cwf=kxzcomp⁡Cwgxycomp⁡Czf
67 3 4 5 7 8 20 36 45 51 66 iscatd2 ⊢φ→C∈Cat∧Id⁡C=y∈BaseC⟼0M