A nonsoluble residually finite, locally finite group with a full prime-support Sylow basis

We construct a countable residually finite, locally finite group \(G\) containing \(\operatorname{Sym}(5)\) and Sylow subgroups \(P_2,P_3,P_5\) such that \(G=\langle P_2,P_3,P_5\rangle\) and \(\langle P_p,P_q\rangle\) is a \(\{p,q\}\)-group whenever \(p\ne q\). Thus \(G\) has a full Sylow basis in Golberg's prime-support sense, although it is not locally soluble. The construction uses finite regular wreath products. A coordinate subgroup enlarges one selected \(p\)-subgroup while preserving the prime supports and intersections of the three pair joins; an element outside the selected subgroup then produces an element of another prime order. Iteration makes the three limit subgroups maximal. The construction and its stated properties are formalised in Lean 4.