section‹Ordinals in generic extensions›
theory Ordinals_In_MG
imports
Forcing_Theorems Relative_Univ
begin
context G_generic
begin
lemma rank_val: "rank(val(G,x)) ≤ rank(x)" (is "?Q(x)")
proof (induct rule:ed_induction[of ?Q])
case (1 x)
have "val(G,x) = {val(G,u). u∈{t∈domain(x). ∃p∈P . <t,p>∈x ∧ p ∈ G }}"
using def_val unfolding Sep_and_Replace by blast
then
have "rank(val(G,x)) = (⋃u∈{t∈domain(x). ∃p∈P . <t,p>∈x ∧ p ∈ G }. succ(rank(val(G,u))))"
using rank[of "val(G,x)"] by simp
moreover
have "succ(rank(val(G, y))) ≤ rank(x)" if "ed(y, x)" for y
using 1[OF that] rank_ed[OF that] by (auto intro:lt_trans1)
moreover from this
have "(⋃u∈{t∈domain(x). ∃p∈P . <t,p>∈x ∧ p ∈ G }. succ(rank(val(G,u)))) ≤ rank(x)"
by (rule_tac UN_least_le) (auto)
ultimately
show ?case by simp
qed
lemma Ord_MG_iff:
assumes "Ord(α)"
shows "α ∈ M ⟷ α ∈ M[G]"
proof
show "α ∈ M ⟹ α ∈ M[G]"
using generic[THEN one_in_G, THEN M_subset_MG] ..
next
assume "α ∈ M[G]"
then
obtain x where "x∈M" "val(G,x) = α"
using GenExtD by auto
then
have "rank(α) ≤ rank(x)"
using rank_val by blast
with assms
have "α ≤ rank(x)"
using rank_of_Ord by simp
then
have "α ∈ succ(rank(x))" using ltD by simp
with ‹x∈M›
show "α ∈ M"
using cons_closed transitivity[of α "succ(rank(x))"]
rank_closed unfolding succ_def by simp
qed
end
end