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}});