I think it's a bit worse than that. The idealization axiom is equivalent to the existence of a finite set containing all standard sets AND plenty of standard sets are infinite, for example, N, Q, R, etc. All the classically constructed sets that are infinite are still infinite in IST. This axiom is something I have also been thinking about. It seems to receive brief discussion in the literature that I have read. It's the sort of thing that if you started a presentation with that sentence, folks would certainly want more information.
The finite set (call it A) containing all standard sets cannot itself be internal because it uses the predicate standard. So it must be an external set. I know that IST isn't able to access external sets (though I can't make that precise) very well. Given that we measure whether a set is finite or infinite with functions I wonder if the issue is whether the function exists. That would require looking at subsets of AxA but that product isn't necessarily guaranteed to exist because transfer only gives us products of standard sets. So can we even construct an injection from A to A in order to determine that it is necessarily surjective?
EDIT: I'm working on these ideas too and so have been thinking about this some more. Within IST the 'usual' natural numbers or 'usual reals' aren't sets and so we might relax our surprise that there is a finite set containing them. Cardinality, I read somewhere, is necessarily an external concept because it depends on the sets available in the model. Additionally, I wonder if there is some equivocation of the use of "finite" which in our everyday language doesn't necessarily match up with the mathematical definition which can be "not infinite" which allows for considerable quantities to be finite (the number of books in the Library of Babel by Jorge Borges) or Graham's number, even those these numbers are...I'm not sure how to say, larger than anything we can reasonably conceptualize.