# Metamath Proof Explorer

## Theorem ablfaclem2

Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Proof shortened by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses ablfac.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
ablfac.c ${⊢}{C}=\left\{{r}\in \mathrm{SubGrp}\left({G}\right)|{G}{↾}_{𝑠}{r}\in \left(\mathrm{CycGrp}\cap \mathrm{ran}\mathrm{pGrp}\right)\right\}$
ablfac.1 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablfac.2 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
ablfac.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
ablfac.a ${⊢}{A}=\left\{{w}\in ℙ|{w}\parallel \left|{B}\right|\right\}$
ablfac.s ${⊢}{S}=\left({p}\in {A}⟼\left\{{x}\in {B}|{O}\left({x}\right)\parallel {{p}}^{{p}\mathrm{pCnt}\left|{B}\right|}\right\}\right)$
ablfac.w ${⊢}{W}=\left({g}\in \mathrm{SubGrp}\left({G}\right)⟼\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={g}\right)\right\}\right)$
ablfaclem2.f ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Word}{C}$
ablfaclem2.q ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\in {W}\left({S}\left({y}\right)\right)$
ablfaclem2.l ${⊢}{L}=\bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×\mathrm{dom}{F}\left({y}\right)\right)$
ablfaclem2.g ${⊢}{\phi }\to {H}:\left(0..^\left|{L}\right|\right)\underset{1-1 onto}{⟶}{L}$
Assertion ablfaclem2 ${⊢}{\phi }\to {W}\left({B}\right)\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 ablfac.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablfac.c ${⊢}{C}=\left\{{r}\in \mathrm{SubGrp}\left({G}\right)|{G}{↾}_{𝑠}{r}\in \left(\mathrm{CycGrp}\cap \mathrm{ran}\mathrm{pGrp}\right)\right\}$
3 ablfac.1 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
4 ablfac.2 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
5 ablfac.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
6 ablfac.a ${⊢}{A}=\left\{{w}\in ℙ|{w}\parallel \left|{B}\right|\right\}$
7 ablfac.s ${⊢}{S}=\left({p}\in {A}⟼\left\{{x}\in {B}|{O}\left({x}\right)\parallel {{p}}^{{p}\mathrm{pCnt}\left|{B}\right|}\right\}\right)$
8 ablfac.w ${⊢}{W}=\left({g}\in \mathrm{SubGrp}\left({G}\right)⟼\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={g}\right)\right\}\right)$
9 ablfaclem2.f ${⊢}{\phi }\to {F}:{A}⟶\mathrm{Word}{C}$
10 ablfaclem2.q ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\in {W}\left({S}\left({y}\right)\right)$
11 ablfaclem2.l ${⊢}{L}=\bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×\mathrm{dom}{F}\left({y}\right)\right)$
12 ablfaclem2.g ${⊢}{\phi }\to {H}:\left(0..^\left|{L}\right|\right)\underset{1-1 onto}{⟶}{L}$
13 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
14 1 subgid ${⊢}{G}\in \mathrm{Grp}\to {B}\in \mathrm{SubGrp}\left({G}\right)$
15 1 2 3 4 5 6 7 8 ablfaclem1 ${⊢}{B}\in \mathrm{SubGrp}\left({G}\right)\to {W}\left({B}\right)=\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)\right\}$
16 3 13 14 15 4syl ${⊢}{\phi }\to {W}\left({B}\right)=\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)\right\}$
17 9 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in \mathrm{Word}{C}$
18 wrdf ${⊢}{F}\left({y}\right)\in \mathrm{Word}{C}\to {F}\left({y}\right):\left(0..^\left|{F}\left({y}\right)\right|\right)⟶{C}$
19 17 18 syl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right):\left(0..^\left|{F}\left({y}\right)\right|\right)⟶{C}$
20 19 ffdmd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right):\mathrm{dom}{F}\left({y}\right)⟶{C}$
21 20 ffvelrnda ${⊢}\left(\left({\phi }\wedge {y}\in {A}\right)\wedge {z}\in \mathrm{dom}{F}\left({y}\right)\right)\to {F}\left({y}\right)\left({z}\right)\in {C}$
22 21 anasss ${⊢}\left({\phi }\wedge \left({y}\in {A}\wedge {z}\in \mathrm{dom}{F}\left({y}\right)\right)\right)\to {F}\left({y}\right)\left({z}\right)\in {C}$
23 22 ralrimivva ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\left({y}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\left({z}\right)\in {C}$
24 eqid ${⊢}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)=\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
25 24 fmpox ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\left({y}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\left({z}\right)\in {C}↔\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):\bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×\mathrm{dom}{F}\left({y}\right)\right)⟶{C}$
26 23 25 sylib ${⊢}{\phi }\to \left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):\bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×\mathrm{dom}{F}\left({y}\right)\right)⟶{C}$
27 11 feq2i ${⊢}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):{L}⟶{C}↔\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):\bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×\mathrm{dom}{F}\left({y}\right)\right)⟶{C}$
28 26 27 sylibr ${⊢}{\phi }\to \left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):{L}⟶{C}$
29 f1of ${⊢}{H}:\left(0..^\left|{L}\right|\right)\underset{1-1 onto}{⟶}{L}\to {H}:\left(0..^\left|{L}\right|\right)⟶{L}$
30 12 29 syl ${⊢}{\phi }\to {H}:\left(0..^\left|{L}\right|\right)⟶{L}$
31 fco ${⊢}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right):{L}⟶{C}\wedge {H}:\left(0..^\left|{L}\right|\right)⟶{L}\right)\to \left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right):\left(0..^\left|{L}\right|\right)⟶{C}$
32 28 30 31 syl2anc ${⊢}{\phi }\to \left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right):\left(0..^\left|{L}\right|\right)⟶{C}$
33 iswrdi ${⊢}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right):\left(0..^\left|{L}\right|\right)⟶{C}\to \left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\in \mathrm{Word}{C}$
34 32 33 syl ${⊢}{\phi }\to \left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\in \mathrm{Word}{C}$
35 10 r19.21bi ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in {W}\left({S}\left({y}\right)\right)$
36 6 ssrab3 ${⊢}{A}\subseteq ℙ$
37 36 a1i ${⊢}{\phi }\to {A}\subseteq ℙ$
38 1 5 7 3 4 37 ablfac1b ${⊢}{\phi }\to {G}\mathrm{dom}\mathrm{DProd}{S}$
39 1 fvexi ${⊢}{B}\in \mathrm{V}$
40 39 rabex ${⊢}\left\{{x}\in {B}|{O}\left({x}\right)\parallel {{p}}^{{p}\mathrm{pCnt}\left|{B}\right|}\right\}\in \mathrm{V}$
41 40 7 dmmpti ${⊢}\mathrm{dom}{S}={A}$
42 41 a1i ${⊢}{\phi }\to \mathrm{dom}{S}={A}$
43 38 42 dprdf2 ${⊢}{\phi }\to {S}:{A}⟶\mathrm{SubGrp}\left({G}\right)$
44 43 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {S}\left({y}\right)\in \mathrm{SubGrp}\left({G}\right)$
45 1 2 3 4 5 6 7 8 ablfaclem1 ${⊢}{S}\left({y}\right)\in \mathrm{SubGrp}\left({G}\right)\to {W}\left({S}\left({y}\right)\right)=\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)\right\}$
46 44 45 syl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {W}\left({S}\left({y}\right)\right)=\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)\right\}$
47 35 46 eleqtrd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in \left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)\right\}$
48 breq2 ${⊢}{s}={F}\left({y}\right)\to \left({G}\mathrm{dom}\mathrm{DProd}{s}↔{G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\right)$
49 oveq2 ${⊢}{s}={F}\left({y}\right)\to {G}\mathrm{DProd}{s}={G}\mathrm{DProd}{F}\left({y}\right)$
50 49 eqeq1d ${⊢}{s}={F}\left({y}\right)\to \left({G}\mathrm{DProd}{s}={S}\left({y}\right)↔{G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)\right)$
51 48 50 anbi12d ${⊢}{s}={F}\left({y}\right)\to \left(\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)↔\left({G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\wedge {G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)\right)\right)$
52 51 elrab ${⊢}{F}\left({y}\right)\in \left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)\right\}↔\left({F}\left({y}\right)\in \mathrm{Word}{C}\wedge \left({G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\wedge {G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)\right)\right)$
53 52 simprbi ${⊢}{F}\left({y}\right)\in \left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={S}\left({y}\right)\right)\right\}\to \left({G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\wedge {G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)\right)$
54 47 53 syl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\wedge {G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)\right)$
55 54 simpld ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)$
56 dprdf ${⊢}{G}\mathrm{dom}\mathrm{DProd}{F}\left({y}\right)\to {F}\left({y}\right):\mathrm{dom}{F}\left({y}\right)⟶\mathrm{SubGrp}\left({G}\right)$
57 55 56 syl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right):\mathrm{dom}{F}\left({y}\right)⟶\mathrm{SubGrp}\left({G}\right)$
58 57 ffvelrnda ${⊢}\left(\left({\phi }\wedge {y}\in {A}\right)\wedge {z}\in \mathrm{dom}{F}\left({y}\right)\right)\to {F}\left({y}\right)\left({z}\right)\in \mathrm{SubGrp}\left({G}\right)$
59 58 anasss ${⊢}\left({\phi }\wedge \left({y}\in {A}\wedge {z}\in \mathrm{dom}{F}\left({y}\right)\right)\right)\to {F}\left({y}\right)\left({z}\right)\in \mathrm{SubGrp}\left({G}\right)$
60 57 feqmptd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)=\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
61 55 60 breqtrd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\mathrm{dom}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
62 43 feqmptd ${⊢}{\phi }\to {S}=\left({y}\in {A}⟼{S}\left({y}\right)\right)$
63 60 oveq2d ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\mathrm{DProd}{F}\left({y}\right)={G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
64 54 simprd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\mathrm{DProd}{F}\left({y}\right)={S}\left({y}\right)$
65 63 64 eqtr3d ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)={S}\left({y}\right)$
66 65 mpteq2dva ${⊢}{\phi }\to \left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)=\left({y}\in {A}⟼{S}\left({y}\right)\right)$
67 62 66 eqtr4d ${⊢}{\phi }\to {S}=\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)$
68 38 67 breqtrd ${⊢}{\phi }\to {G}\mathrm{dom}\mathrm{DProd}\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)$
69 59 61 68 dprd2d2 ${⊢}{\phi }\to \left({G}\mathrm{dom}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\wedge {G}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)={G}\mathrm{DProd}\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)\right)$
70 69 simpld ${⊢}{\phi }\to {G}\mathrm{dom}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
71 28 fdmd ${⊢}{\phi }\to \mathrm{dom}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)={L}$
72 70 71 12 dprdf1o ${⊢}{\phi }\to \left({G}\mathrm{dom}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)\wedge {G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={G}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)$
73 72 simpld ${⊢}{\phi }\to {G}\mathrm{dom}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)$
74 72 simprd ${⊢}{\phi }\to {G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={G}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)$
75 69 simprd ${⊢}{\phi }\to {G}\mathrm{DProd}\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)={G}\mathrm{DProd}\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)$
76 67 oveq2d ${⊢}{\phi }\to {G}\mathrm{DProd}{S}={G}\mathrm{DProd}\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)$
77 ssidd ${⊢}{\phi }\to {A}\subseteq {A}$
78 1 5 7 3 4 37 6 77 ablfac1c ${⊢}{\phi }\to {G}\mathrm{DProd}{S}={B}$
79 76 78 eqtr3d ${⊢}{\phi }\to {G}\mathrm{DProd}\left({y}\in {A}⟼{G}\mathrm{DProd}\left({z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\right)={B}$
80 74 75 79 3eqtrd ${⊢}{\phi }\to {G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={B}$
81 breq2 ${⊢}{s}=\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\to \left({G}\mathrm{dom}\mathrm{DProd}{s}↔{G}\mathrm{dom}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)\right)$
82 oveq2 ${⊢}{s}=\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\to {G}\mathrm{DProd}{s}={G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)$
83 82 eqeq1d ${⊢}{s}=\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\to \left({G}\mathrm{DProd}{s}={B}↔{G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={B}\right)$
84 81 83 anbi12d ${⊢}{s}=\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\to \left(\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)↔\left({G}\mathrm{dom}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)\wedge {G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={B}\right)\right)$
85 84 rspcev ${⊢}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\in \mathrm{Word}{C}\wedge \left({G}\mathrm{dom}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)\wedge {G}\mathrm{DProd}\left(\left({y}\in {A},{z}\in \mathrm{dom}{F}\left({y}\right)⟼{F}\left({y}\right)\left({z}\right)\right)\circ {H}\right)={B}\right)\right)\to \exists {s}\in \mathrm{Word}{C}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)$
86 34 73 80 85 syl12anc ${⊢}{\phi }\to \exists {s}\in \mathrm{Word}{C}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)$
87 rabn0 ${⊢}\left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)\right\}\ne \varnothing ↔\exists {s}\in \mathrm{Word}{C}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)$
88 86 87 sylibr ${⊢}{\phi }\to \left\{{s}\in \mathrm{Word}{C}|\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={B}\right)\right\}\ne \varnothing$
89 16 88 eqnetrd ${⊢}{\phi }\to {W}\left({B}\right)\ne \varnothing$