Fix . In the ambient universe form the setby 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 thatThis 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. Thereforewhich 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
There are currently no matching articles.