Theory Ordinals_In_MG
section‹Ordinals in generic extensions›
theory Ordinals_In_MG
imports
Forcing_Theorems
begin
context G_generic1
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∈G . ⟨t,p⟩∈x }}"
using def_val[of G x] by auto
then
have "rank(val(G,x)) = (⋃u∈{t∈domain(x). ∃p∈G . ⟨t,p⟩∈x }. 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∈G . ⟨t,p⟩∈x }. 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[G]" if "α ∈ M"
using M_subset_MG[OF one_in_G] that ..
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