Fix . In the ambient universe form the set
by power set and separation, using definability of . This is the collection which must serve as the power set of inside ; it need not be the entire ambient power set.
For each , let be the least ordinal with . Ambient replacement is used to collect the ordinals into a set. Their supremum, enlarged if necessary to include a stage containing , gives an ordinal such that and every belongs to .
Because is transitive and , the bounded property for has its actual meaning when evaluated in that structure: every element of already lies in , and membership is unchanged. It follows that
This is a definable subset of using the parameter , so . Every member of which is a subset of is in , and every member of is such a subset. Therefore
which is exactly the power-set axiom in . The replacement step is indispensable to this proof: definability over one stage requires first bounding all the constructible subsets by one common stage.

Articles by others on the same topic (0)

There are currently no matching articles.