src/ZF/Constructible/Relative.thy
 changeset 13319 23de7b3af453 parent 13316 d16629fd0f95 child 13323 2c287f50c9f3
```     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:41 2002 +0200
1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:53 2002 +0200
1.3 @@ -764,9 +764,13 @@
1.4  	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
1.5  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
1.6    and is_recfun_separation:
1.7 -     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
1.8 -     "[| M(A); M(f); M(g); M(a); M(b) |]
1.9 -     ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
1.10 +     --{*for well-founded recursion*}
1.11 +     "[| M(r); M(f); M(g); M(a); M(b) |]
1.12 +     ==> separation(M,
1.13 +            \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
1.14 +                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
1.15 +                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
1.16 +                                   fx \<noteq> gx))"
1.17
1.18  lemma (in M_axioms) cartprod_iff_lemma:
1.19       "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
```