The large structures of Grothendieck founded on finite-order arithmetic