ZFC without Power Set, effect of adding well ordering or not. As $\mathsf{ZFC}$ axioms:

*

*set existence

*extensionality

*foundation

*restricted comprehension

*pairing

*union

*collection (instead of replacement)

*infinity

*power set ($\mathsf{Pow}$)

*well ordering ($\mathsf{AC}$)

I call $\mathsf{ZFC}$ the theory with {1,...,10},
$\mathsf{ZF}$ the theory with {1,...9}
$\mathsf{ZFC}$-{power set} is equivalent to $\mathsf{ZF}$-{power set} ?
What is the effect of adding well-ordering into $\mathsf{ZF}$-{power set}?
Intuitively it seems that without Power Set we don't have uncountable sets, so every infinite set would be enumerable, and this bijection could provide a well-order.
I am almost sure that well-ordering has no effect into {1-7}.
UPDATE: Add some format. Not sure if it makes a lot of diference but I took collection instead of replacement because of this (Which set theories without the power set axiom are used occasionally?)
 A: If $\mathcal{M}\models\mathsf{ZF-Pow}$, then $\mathsf{HC}^\mathcal{M}$ (= the substructure of $\mathcal{M}$ consisting of all objects which $\mathcal{M}$ thinks are hereditarily countable sets) is a model of $\mathsf{ZFC-Pow}$ + "Every set is countable." This can be verified in a very weak set theory (e.g. $\mathsf{KP}$) or reformulated in terms of consistency and proved in arithmetic (e.g. $\mathsf{I\Sigma_1}$). Consequently:

*

*In a precise sense, we do need powerset to prove the existence of an uncountable set: $\mathsf{ZFC-Pow}$ has models satisfying "Every set is countable" (assuming it is consistent in the first place). Dropping choice has nothing to do with this (although adding the negation of choice does - every countable set is a fortiori well-orderable, so $\mathsf{ZF+\neg AC}$ does prove that there is an uncountable set). Of course, even $\mathsf{ZFC-Pow+\neg Pow}$ is still consistent with "There is an uncountable set," so your statement "without powerset we don't have uncountable sets" is still incorrect.


*In terms of consistency strength, there's no difference between $\mathsf{ZF-Pow}$, $\mathsf{ZFC-Pow}$, and $\mathsf{ZFC-Pow}$ + "Every set is countable."
Interestingly, showing that $\mathsf{ZF-Pow}\not\vdash \mathsf{AC}$ is a bit more nuanced. Certainly (by Cohen) this is a consequence of $\mathsf{Con(ZF)}$, but this is rather overkill-y; can we get by just assuming $\mathsf{Con(ZF-Pow)}$ (which is a much weaker assumption)?
Embarrassingly, I don't see how to do this! The issue is that models of $\mathsf{ZF-Pow}$ can be "too small" for the symmetric extension technique to work properly. Specifically, let $\alpha$ be the second smallest ordinal such that $L_\alpha\models\mathsf{ZFC-Pow}$. Then - unless I'm getting things wrong - $L_\alpha\models$ "$\mathsf{ZFC-Pow}$ has a transitive model but $\mathsf{ZF-Pow+\neg AC}$ does not have a transitive model." This shows that any argument for establishing the consistency of $\mathsf{ZF-Pow+\neg AC}$ relative to that of $\mathsf{ZF-Pow}$ over a not-too-strong base theory must crucially involve non-well-founded constructions.
