In the Basic Fraenkel Model (BFM), ZFA in Jech's book "The Axiom of Choice", permutations in a group are used to define a normal filter. My question is:
- Do these permutations need to be in the BFM model (i.e have finite support)? Or do they come from the bigger class, ZFA + AC? (it is not clear to me from the text).
If the answer is that they come from the bigger model, then this leads to a follow-up question:
- Is it known if the Basic Fraenkel Model defined using the group of all permutations on atoms $A$ is equivalent to a model which is defined similarly except that it uses the group of permutations on $A$ which moves only finitely many atoms?
Thanks in advance for any clarity on this!