Theory Ordinals_In_MG

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 (* G_generic *)

end