src/ZF/Constructible/Wellorderings.thy
 changeset 13295 ca2e9b273472 parent 13293 09276ee04361 child 13298 b4f370679c65
equal 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 |]`