Metamath Proof Explorer


Theorem estrccatid

Description: Lemma for estrccat . (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypothesis estrccat.c C=ExtStrCatU
Assertion estrccatid UVCCatIdC=xUIBasex

Proof

Step Hyp Ref Expression
1 estrccat.c C=ExtStrCatU
2 id UVUV
3 1 2 estrcbas UVU=BaseC
4 eqidd UVHomC=HomC
5 eqidd UVcompC=compC
6 1 fvexi CV
7 6 a1i UVCV
8 biid wUxUyUzUfwHomCxgxHomCyhyHomCzwUxUyUzUfwHomCxgxHomCyhyHomCz
9 f1oi IBasex:Basex1-1 ontoBasex
10 f1of IBasex:Basex1-1 ontoBasexIBasex:BasexBasex
11 9 10 mp1i UVxUIBasex:BasexBasex
12 simpl UVxUUV
13 eqid HomC=HomC
14 simpr UVxUxU
15 eqid Basex=Basex
16 1 12 13 14 14 15 15 elestrchom UVxUIBasexxHomCxIBasex:BasexBasex
17 11 16 mpbird UVxUIBasexxHomCx
18 simpl UVwUxUyUzUfwHomCxgxHomCyhyHomCzUV
19 eqid compC=compC
20 simpr1l UVwUxUyUzUfwHomCxgxHomCyhyHomCzwU
21 simpr1r UVwUxUyUzUfwHomCxgxHomCyhyHomCzxU
22 eqid Basew=Basew
23 simpr31 UVwUxUyUzUfwHomCxgxHomCyhyHomCzfwHomCx
24 1 18 13 20 21 22 15 elestrchom UVwUxUyUzUfwHomCxgxHomCyhyHomCzfwHomCxf:BasewBasex
25 23 24 mpbid UVwUxUyUzUfwHomCxgxHomCyhyHomCzf:BasewBasex
26 9 10 mp1i UVwUxUyUzUfwHomCxgxHomCyhyHomCzIBasex:BasexBasex
27 1 18 19 20 21 21 22 15 15 25 26 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzIBasexwxcompCxf=IBasexf
28 fcoi2 f:BasewBasexIBasexf=f
29 25 28 syl UVwUxUyUzUfwHomCxgxHomCyhyHomCzIBasexf=f
30 27 29 eqtrd UVwUxUyUzUfwHomCxgxHomCyhyHomCzIBasexwxcompCxf=f
31 simpr2l UVwUxUyUzUfwHomCxgxHomCyhyHomCzyU
32 eqid Basey=Basey
33 simpr32 UVwUxUyUzUfwHomCxgxHomCyhyHomCzgxHomCy
34 1 18 13 21 31 15 32 elestrchom UVwUxUyUzUfwHomCxgxHomCyhyHomCzgxHomCyg:BasexBasey
35 33 34 mpbid UVwUxUyUzUfwHomCxgxHomCyhyHomCzg:BasexBasey
36 1 18 19 21 21 31 15 15 32 26 35 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzgxxcompCyIBasex=gIBasex
37 fcoi1 g:BasexBaseygIBasex=g
38 35 37 syl UVwUxUyUzUfwHomCxgxHomCyhyHomCzgIBasex=g
39 36 38 eqtrd UVwUxUyUzUfwHomCxgxHomCyhyHomCzgxxcompCyIBasex=g
40 1 18 19 20 21 31 22 15 32 25 35 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzgwxcompCyf=gf
41 fco g:BasexBaseyf:BasewBasexgf:BasewBasey
42 35 25 41 syl2anc UVwUxUyUzUfwHomCxgxHomCyhyHomCzgf:BasewBasey
43 1 18 13 20 31 22 32 elestrchom UVwUxUyUzUfwHomCxgxHomCyhyHomCzgfwHomCygf:BasewBasey
44 42 43 mpbird UVwUxUyUzUfwHomCxgxHomCyhyHomCzgfwHomCy
45 40 44 eqeltrd UVwUxUyUzUfwHomCxgxHomCyhyHomCzgwxcompCyfwHomCy
46 coass hgf=hgf
47 simpr2r UVwUxUyUzUfwHomCxgxHomCyhyHomCzzU
48 eqid Basez=Basez
49 simpr33 UVwUxUyUzUfwHomCxgxHomCyhyHomCzhyHomCz
50 1 18 13 31 47 32 48 elestrchom UVwUxUyUzUfwHomCxgxHomCyhyHomCzhyHomCzh:BaseyBasez
51 49 50 mpbid UVwUxUyUzUfwHomCxgxHomCyhyHomCzh:BaseyBasez
52 fco h:BaseyBasezg:BasexBaseyhg:BasexBasez
53 51 35 52 syl2anc UVwUxUyUzUfwHomCxgxHomCyhyHomCzhg:BasexBasez
54 1 18 19 20 21 47 22 15 48 25 53 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzhgwxcompCzf=hgf
55 1 18 19 20 31 47 22 32 48 42 51 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzhwycompCzgf=hgf
56 46 54 55 3eqtr4a UVwUxUyUzUfwHomCxgxHomCyhyHomCzhgwxcompCzf=hwycompCzgf
57 1 18 19 21 31 47 15 32 48 35 51 estrcco UVwUxUyUzUfwHomCxgxHomCyhyHomCzhxycompCzg=hg
58 57 oveq1d UVwUxUyUzUfwHomCxgxHomCyhyHomCzhxycompCzgwxcompCzf=hgwxcompCzf
59 40 oveq2d UVwUxUyUzUfwHomCxgxHomCyhyHomCzhwycompCzgwxcompCyf=hwycompCzgf
60 56 58 59 3eqtr4d UVwUxUyUzUfwHomCxgxHomCyhyHomCzhxycompCzgwxcompCzf=hwycompCzgwxcompCyf
61 3 4 5 7 8 17 30 39 45 60 iscatd2 UVCCatIdC=xUIBasex