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{tdomain(x). pP .  t,px  p  G }}"
    using def_val unfolding Sep_and_Replace by blast
  then
  have "rank(val(G,x)) = (u{tdomain(x). pP .  t,px  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{tdomain(x). pP .  t,px  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 "xM" "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 xM
  show "α  M"
    using cons_closed transitivity[of α "succ(rank(x))"] 
      rank_closed unfolding succ_def by simp  
qed
  
end (* G_generic *)

end