Page 73 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 65
Proof . Note that the formula φ may contain further free parameters, which we do not mention for the sake of simplicity. Assume that ∀u, v, v′((φ(u, v) ∧ φ(u,v′)) → v ≡ v′) and let x = (x,Rx) be a point. Let A = {i|iRx x}. For each i ∈ A we have the point (i,Rx) ◭ (x,Rx) = x. Using replacement and choice in SO we can pick for each i ∈ A a point zi = (zi,Rzi) such that φ((i,Rx),zi) holds if such a point exists. By the comprehension Lemma 7.1 there is a point y = (y,Ry) such that for all points z
z ◭ y ↔ ∃i ∈ Az ≡ zi.
To show the instance of the replacement schema under consideration, assume that z ◭ y. Take i ∈ A such that z ≡ zi. Then (i,Rx) ◭ (x,Rx) = x, φ((i, Rx), zi) and φ((i, Rx), z). Hence ∃u(u ◭ x ∧ φ(u, z)).
Conversely, assume that ∃u(u ◭ x∧φ(u,z)). Take u ◭ x such that φ(u,z). Take i Rx x, i ∈ A such that u ≡ (i, Rx). Then φ((i, Rx), z). By definition of zi, φ((i,Rx),zi). The functionality of the formula φ implies z ≡ zi. Hence
∃i∈Az≡zi andz◭y.
The replacement schema also implies the separation schema.
(5) The axiom of powersets holds in :
∀x∃y∀z(z ◭ y ↔ ∀w(w ◭ z → w ◭ x)).
Proof . By the separation schema it suffices to show that ∀x∃y∀c(∀w(w ◭ c → w ◭ x) → c ◭ y).
qed(4)
Consider a point x = (x, Rx). Let F = dom(Rx) ∪ ran(Rx) be the field of Rx. By the powerset axiom of SO choose some set P such that Pow(P, F ):
∀z(∃α(α ∈ z) ∧ ∀α(α ∈ z → α ∈ F ) → ∃ξ∀β(β ∈ z ↔ (β, ξ) ∈ P )). Choose two large ordinals δ and y such that
∀α ∈ Fα < δ and ∀ξ(ξ ∈ ran(P) → (δ,ξ) < y). Define a point y = (y,Ry) by
Ry = Rx ∪{(β,(δ,ξ))|(β,ξ) ∈ P}∪{((δ,ξ),y)|ξ ∈ ran(P)}.
To show the axiom consider some point c = (c,Rc) such that ∀w(w◭c→w◭x).
Define a corresponding subset z of F by
z = {β ∈ F|∃vRcc(v,Rc) ≡ (β,Rx)}.
We may assume for simplicity that z ̸= ∅. By the powerset axiom of SO choose ξ ∈ ran(P ) such that
∀β(β ∈ z ↔ (β,ξ) ∈ P).