src/ZF/Constructible/Wellorderings.thy
changeset 13295 ca2e9b273472
parent 13293 09276ee04361
child 13298 b4f370679c65
equal deleted inserted replaced
13294:5e2016d151bd 13295:ca2e9b273472
   293      "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   293      "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   294 by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
   294 by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
   295 
   295 
   296 
   296 
   297 text{*Surely a shorter proof using lemmas in @{text Order}?
   297 text{*Surely a shorter proof using lemmas in @{text Order}?
   298      Like well_ord_iso_preserving?*}
   298      Like @{text well_ord_iso_preserving}?*}
   299 lemma (in M_axioms) ord_iso_pred_imp_lt:
   299 lemma (in M_axioms) ord_iso_pred_imp_lt:
   300      "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   300      "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   301        g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   301        g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   302        wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   302        wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   303        Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
   303        Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]