# Metamath Proof Explorer

## Theorem funcestrcsetclem9

Description: Lemma 9 for funcestrcsetc . (Contributed by AV, 23-Mar-2020)

Ref Expression
Hypotheses funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
Assertion funcestrcsetclem9 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\wedge \left({H}\in \left({X}\mathrm{Hom}\left({E}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({E}\right){Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$

### Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
2 funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
3 funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
4 funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
5 funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
6 funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
7 funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
8 5 adantr ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {U}\in \mathrm{WUni}$
9 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
10 1 5 estrcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{E}}$
11 10 3 syl6reqr ${⊢}{\phi }\to {B}={U}$
12 11 eleq2d ${⊢}{\phi }\to \left({X}\in {B}↔{X}\in {U}\right)$
13 12 biimpcd ${⊢}{X}\in {B}\to \left({\phi }\to {X}\in {U}\right)$
14 13 3ad2ant1 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {X}\in {U}\right)$
15 14 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {U}$
16 11 eleq2d ${⊢}{\phi }\to \left({Y}\in {B}↔{Y}\in {U}\right)$
17 16 biimpcd ${⊢}{Y}\in {B}\to \left({\phi }\to {Y}\in {U}\right)$
18 17 3ad2ant2 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {Y}\in {U}\right)$
19 18 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {U}$
20 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
21 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
22 1 8 9 15 19 20 21 estrchom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\mathrm{Hom}\left({E}\right){Y}={{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}$
23 22 eleq2d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({H}\in \left({X}\mathrm{Hom}\left({E}\right){Y}\right)↔{H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)$
24 11 eleq2d ${⊢}{\phi }\to \left({Z}\in {B}↔{Z}\in {U}\right)$
25 24 biimpcd ${⊢}{Z}\in {B}\to \left({\phi }\to {Z}\in {U}\right)$
26 25 3ad2ant3 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {Z}\in {U}\right)$
27 26 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {U}$
28 eqid ${⊢}{\mathrm{Base}}_{{Z}}={\mathrm{Base}}_{{Z}}$
29 1 8 9 19 27 21 28 estrchom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\mathrm{Hom}\left({E}\right){Z}={{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}$
30 29 eleq2d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({K}\in \left({Y}\mathrm{Hom}\left({E}\right){Z}\right)↔{K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)$
31 23 30 anbi12d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({X}\mathrm{Hom}\left({E}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({E}\right){Z}\right)\right)↔\left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)$
32 elmapi ${⊢}{K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\to {K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}$
33 elmapi ${⊢}{H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\to {H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
34 fco ${⊢}\left({K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}\wedge {H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)\to \left({K}\circ {H}\right):{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Z}}$
35 32 33 34 syl2an ${⊢}\left({K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\wedge {H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)\to \left({K}\circ {H}\right):{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Z}}$
36 fvex ${⊢}{\mathrm{Base}}_{{Z}}\in \mathrm{V}$
37 fvex ${⊢}{\mathrm{Base}}_{{X}}\in \mathrm{V}$
38 36 37 elmap ${⊢}{K}\circ {H}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)↔\left({K}\circ {H}\right):{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Z}}$
39 35 38 sylibr ${⊢}\left({K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\wedge {H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)\to {K}\circ {H}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)$
40 39 ancoms ${⊢}\left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\to {K}\circ {H}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)$
41 40 adantl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {K}\circ {H}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)$
42 fvresi ${⊢}{K}\circ {H}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)\to \left({\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}\right)\left({K}\circ {H}\right)={K}\circ {H}$
43 41 42 syl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}\right)\left({K}\circ {H}\right)={K}\circ {H}$
44 1 2 3 4 5 6 7 20 28 funcestrcsetclem5 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}$
45 44 3adantr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}$
46 45 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}$
47 8 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {U}\in \mathrm{WUni}$
48 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
49 15 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {X}\in {U}$
50 19 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {Y}\in {U}$
51 27 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {Z}\in {U}$
52 33 ad2antrl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
53 32 ad2antll ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}$
54 1 47 48 49 50 51 20 21 28 52 53 estrcco ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}={K}\circ {H}$
55 46 54 fveq12d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{X}}}\right)}\right)\left({K}\circ {H}\right)$
56 eqid ${⊢}\mathrm{comp}\left({S}\right)=\mathrm{comp}\left({S}\right)$
57 1 2 3 4 5 6 funcestrcsetclem2 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in {U}$
58 57 3ad2antr1 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({X}\right)\in {U}$
59 58 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {F}\left({X}\right)\in {U}$
60 1 2 3 4 5 6 funcestrcsetclem2 ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)\in {U}$
61 60 3ad2antr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Y}\right)\in {U}$
62 61 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {F}\left({Y}\right)\in {U}$
63 1 2 3 4 5 6 funcestrcsetclem2 ${⊢}\left({\phi }\wedge {Z}\in {B}\right)\to {F}\left({Z}\right)\in {U}$
64 63 3ad2antr3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Z}\right)\in {U}$
65 64 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {F}\left({Z}\right)\in {U}$
66 1 2 3 4 5 6 funcestrcsetclem1 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
67 66 3ad2antr1 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
68 1 2 3 4 5 6 funcestrcsetclem1 ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
69 68 3ad2antr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
70 67 69 feq23d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({H}:{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)$
71 70 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({H}:{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)$
72 52 71 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {H}:{F}\left({X}\right)⟶{F}\left({Y}\right)$
73 simpll ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {\phi }$
74 3simpa ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
75 74 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
76 simprl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)$
77 1 2 3 4 5 6 7 20 21 funcestrcsetclem6 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$
78 73 75 76 77 syl3anc ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$
79 78 feq1d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left(\left({X}{G}{Y}\right)\left({H}\right):{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{F}\left({X}\right)⟶{F}\left({Y}\right)\right)$
80 72 79 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right):{F}\left({X}\right)⟶{F}\left({Y}\right)$
81 1 2 3 4 5 6 funcestrcsetclem1 ${⊢}\left({\phi }\wedge {Z}\in {B}\right)\to {F}\left({Z}\right)={\mathrm{Base}}_{{Z}}$
82 81 3ad2antr3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Z}\right)={\mathrm{Base}}_{{Z}}$
83 69 82 feq23d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}\right)$
84 83 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}\right)$
85 53 84 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)$
86 3simpc ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({Y}\in {B}\wedge {Z}\in {B}\right)$
87 86 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}\in {B}\wedge {Z}\in {B}\right)$
88 simprr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)$
89 1 2 3 4 5 6 7 21 28 funcestrcsetclem6 ${⊢}\left({\phi }\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)={K}$
90 73 87 88 89 syl3anc ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)={K}$
91 90 feq1d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left(\left({Y}{G}{Z}\right)\left({K}\right):{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)\right)$
92 85 91 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right):{F}\left({Y}\right)⟶{F}\left({Z}\right)$
93 2 47 56 59 62 65 80 92 setcco ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\circ \left({X}{G}{Y}\right)\left({H}\right)$
94 90 78 coeq12d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\circ \left({X}{G}{Y}\right)\left({H}\right)={K}\circ {H}$
95 93 94 eqtrd ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)={K}\circ {H}$
96 43 55 95 3eqtr4d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$
97 96 ex ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\wedge {K}\in \left({{\mathrm{Base}}_{{Z}}}^{{\mathrm{Base}}_{{Y}}}\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)\right)$
98 31 97 sylbid ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({X}\mathrm{Hom}\left({E}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({E}\right){Z}\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)\right)$
99 98 3impia ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\wedge \left({H}\in \left({X}\mathrm{Hom}\left({E}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({E}\right){Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({E}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$