Metamath Proof Explorer

Theorem funcestrcsetclem9

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

Ref Expression
Hypotheses funcestrcsetc.e ⊢E=ExtStrCat⁡U
funcestrcsetc.s ⊢S=SetCat⁡U
funcestrcsetc.b ⊢B=BaseE
funcestrcsetc.c ⊢C=BaseS
funcestrcsetc.u ⊢φ→U∈WUni
funcestrcsetc.f ⊢φ→F=x∈B⟼Basex
funcestrcsetc.g ⊢φ→G=x∈B,y∈B⟼I↾BaseyBasex
Assertion funcestrcsetclem9 ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈XHom⁡EY∧K∈YHom⁡EZ→XGZ⁡KXYcomp⁡EZH=YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ⊢E=ExtStrCat⁡U
2 funcestrcsetc.s ⊢S=SetCat⁡U
3 funcestrcsetc.b ⊢B=BaseE
4 funcestrcsetc.c ⊢C=BaseS
5 funcestrcsetc.u ⊢φ→U∈WUni
6 funcestrcsetc.f ⊢φ→F=x∈B⟼Basex
7 funcestrcsetc.g ⊢φ→G=x∈B,y∈B⟼I↾BaseyBasex
8 5 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B→U∈WUni
9 eqid ⊢Hom⁡E=Hom⁡E
10 1 5 estrcbas ⊢φ→U=BaseE
11 3 10 eqtr4id ⊢φ→B=U
12 11 eleq2d ⊢φ→X∈B↔X∈U
13 12 biimpcd ⊢X∈B→φ→X∈U
14 13 3ad2ant1 ⊢X∈B∧Y∈B∧Z∈B→φ→X∈U
15 14 impcom ⊢φ∧X∈B∧Y∈B∧Z∈B→X∈U
16 11 eleq2d ⊢φ→Y∈B↔Y∈U
17 16 biimpcd ⊢Y∈B→φ→Y∈U
18 17 3ad2ant2 ⊢X∈B∧Y∈B∧Z∈B→φ→Y∈U
19 18 impcom ⊢φ∧X∈B∧Y∈B∧Z∈B→Y∈U
20 eqid ⊢BaseX=BaseX
21 eqid ⊢BaseY=BaseY
22 1 8 9 15 19 20 21 estrchom ⊢φ∧X∈B∧Y∈B∧Z∈B→XHom⁡EY=BaseYBaseX
23 22 eleq2d ⊢φ∧X∈B∧Y∈B∧Z∈B→H∈XHom⁡EY↔H∈BaseYBaseX
24 11 eleq2d ⊢φ→Z∈B↔Z∈U
25 24 biimpcd ⊢Z∈B→φ→Z∈U
26 25 3ad2ant3 ⊢X∈B∧Y∈B∧Z∈B→φ→Z∈U
27 26 impcom ⊢φ∧X∈B∧Y∈B∧Z∈B→Z∈U
28 eqid ⊢BaseZ=BaseZ
29 1 8 9 19 27 21 28 estrchom ⊢φ∧X∈B∧Y∈B∧Z∈B→YHom⁡EZ=BaseZBaseY
30 29 eleq2d ⊢φ∧X∈B∧Y∈B∧Z∈B→K∈YHom⁡EZ↔K∈BaseZBaseY
31 23 30 anbi12d ⊢φ∧X∈B∧Y∈B∧Z∈B→H∈XHom⁡EY∧K∈YHom⁡EZ↔H∈BaseYBaseX∧K∈BaseZBaseY
32 elmapi ⊢K∈BaseZBaseY→K:BaseY⟶BaseZ
33 elmapi ⊢H∈BaseYBaseX→H:BaseX⟶BaseY
34 fco ⊢K:BaseY⟶BaseZ∧H:BaseX⟶BaseY→K∘H:BaseX⟶BaseZ
35 32 33 34 syl2an ⊢K∈BaseZBaseY∧H∈BaseYBaseX→K∘H:BaseX⟶BaseZ
36 fvex ⊢BaseZ∈V
37 fvex ⊢BaseX∈V
38 36 37 elmap ⊢K∘H∈BaseZBaseX↔K∘H:BaseX⟶BaseZ
39 35 38 sylibr ⊢K∈BaseZBaseY∧H∈BaseYBaseX→K∘H∈BaseZBaseX
40 39 ancoms ⊢H∈BaseYBaseX∧K∈BaseZBaseY→K∘H∈BaseZBaseX
41 40 adantl ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→K∘H∈BaseZBaseX
42 fvresi ⊢K∘H∈BaseZBaseX→I↾BaseZBaseX⁡K∘H=K∘H
43 41 42 syl ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→I↾BaseZBaseX⁡K∘H=K∘H
44 1 2 3 4 5 6 7 20 28 funcestrcsetclem5 ⊢φ∧X∈B∧Z∈B→XGZ=I↾BaseZBaseX
45 44 3adantr2 ⊢φ∧X∈B∧Y∈B∧Z∈B→XGZ=I↾BaseZBaseX
46 45 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGZ=I↾BaseZBaseX
47 8 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→U∈WUni
48 eqid ⊢comp⁡E=comp⁡E
49 15 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→X∈U
50 19 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→Y∈U
51 27 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→Z∈U
52 33 ad2antrl ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→H:BaseX⟶BaseY
53 32 ad2antll ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→K:BaseY⟶BaseZ
54 1 47 48 49 50 51 20 21 28 52 53 estrcco ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→KXYcomp⁡EZH=K∘H
55 46 54 fveq12d ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGZ⁡KXYcomp⁡EZH=I↾BaseZBaseX⁡K∘H
56 eqid ⊢comp⁡S=comp⁡S
57 1 2 3 4 5 6 funcestrcsetclem2 ⊢φ∧X∈B→F⁡X∈U
58 57 3ad2antr1 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡X∈U
59 58 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→F⁡X∈U
60 1 2 3 4 5 6 funcestrcsetclem2 ⊢φ∧Y∈B→F⁡Y∈U
61 60 3ad2antr2 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡Y∈U
62 61 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→F⁡Y∈U
63 1 2 3 4 5 6 funcestrcsetclem2 ⊢φ∧Z∈B→F⁡Z∈U
64 63 3ad2antr3 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡Z∈U
65 64 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→F⁡Z∈U
66 1 2 3 4 5 6 funcestrcsetclem1 ⊢φ∧X∈B→F⁡X=BaseX
67 66 3ad2antr1 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡X=BaseX
68 1 2 3 4 5 6 funcestrcsetclem1 ⊢φ∧Y∈B→F⁡Y=BaseY
69 68 3ad2antr2 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡Y=BaseY
70 67 69 feq23d ⊢φ∧X∈B∧Y∈B∧Z∈B→H:F⁡X⟶F⁡Y↔H:BaseX⟶BaseY
71 70 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→H:F⁡X⟶F⁡Y↔H:BaseX⟶BaseY
72 52 71 mpbird ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→H:F⁡X⟶F⁡Y
73 simpll ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→φ
74 3simpa ⊢X∈B∧Y∈B∧Z∈B→X∈B∧Y∈B
75 74 ad2antlr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→X∈B∧Y∈B
76 simprl ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→H∈BaseYBaseX
77 1 2 3 4 5 6 7 20 21 funcestrcsetclem6 ⊢φ∧X∈B∧Y∈B∧H∈BaseYBaseX→XGY⁡H=H
78 73 75 76 77 syl3anc ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGY⁡H=H
79 78 feq1d ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGY⁡H:F⁡X⟶F⁡Y↔H:F⁡X⟶F⁡Y
80 72 79 mpbird ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGY⁡H:F⁡X⟶F⁡Y
81 1 2 3 4 5 6 funcestrcsetclem1 ⊢φ∧Z∈B→F⁡Z=BaseZ
82 81 3ad2antr3 ⊢φ∧X∈B∧Y∈B∧Z∈B→F⁡Z=BaseZ
83 69 82 feq23d ⊢φ∧X∈B∧Y∈B∧Z∈B→K:F⁡Y⟶F⁡Z↔K:BaseY⟶BaseZ
84 83 adantr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→K:F⁡Y⟶F⁡Z↔K:BaseY⟶BaseZ
85 53 84 mpbird ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→K:F⁡Y⟶F⁡Z
86 3simpc ⊢X∈B∧Y∈B∧Z∈B→Y∈B∧Z∈B
87 86 ad2antlr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→Y∈B∧Z∈B
88 simprr ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→K∈BaseZBaseY
89 1 2 3 4 5 6 7 21 28 funcestrcsetclem6 ⊢φ∧Y∈B∧Z∈B∧K∈BaseZBaseY→YGZ⁡K=K
90 73 87 88 89 syl3anc ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡K=K
91 90 feq1d ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡K:F⁡Y⟶F⁡Z↔K:F⁡Y⟶F⁡Z
92 85 91 mpbird ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡K:F⁡Y⟶F⁡Z
93 2 47 56 59 62 65 80 92 setcco ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H=YGZ⁡K∘XGY⁡H
94 90 78 coeq12d ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡K∘XGY⁡H=K∘H
95 93 94 eqtrd ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H=K∘H
96 43 55 95 3eqtr4d ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈BaseYBaseX∧K∈BaseZBaseY→XGZ⁡KXYcomp⁡EZH=YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H
97 96 ex ⊢φ∧X∈B∧Y∈B∧Z∈B→H∈BaseYBaseX∧K∈BaseZBaseY→XGZ⁡KXYcomp⁡EZH=YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H
98 31 97 sylbid ⊢φ∧X∈B∧Y∈B∧Z∈B→H∈XHom⁡EY∧K∈YHom⁡EZ→XGZ⁡KXYcomp⁡EZH=YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H
99 98 3impia ⊢φ∧X∈B∧Y∈B∧Z∈B∧H∈XHom⁡EY∧K∈YHom⁡EZ→XGZ⁡KXYcomp⁡EZH=YGZ⁡KF⁡XF⁡Ycomp⁡SF⁡ZXGY⁡H