equal
deleted
inserted
replaced
72 |
72 |
73 (*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord |
73 (*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord |
74 The smaller ordinal is an initial segment of the larger *) |
74 The smaller ordinal is an initial segment of the larger *) |
75 lemma lt_pred_Memrel: |
75 lemma lt_pred_Memrel: |
76 "j<i ==> pred(i, j, Memrel(i)) = j" |
76 "j<i ==> pred(i, j, Memrel(i)) = j" |
77 apply (unfold pred_def lt_def) |
77 apply (simp add: pred_def lt_def) |
78 apply (simp (no_asm_simp)) |
|
79 apply (blast intro: Ord_trans) |
78 apply (blast intro: Ord_trans) |
80 done |
79 done |
81 |
80 |
82 lemma pred_Memrel: |
81 lemma pred_Memrel: |
83 "x:A ==> pred(A, x, Memrel(A)) = A \<inter> x" |
82 "x:A ==> pred(A, x, Memrel(A)) = A \<inter> x" |