src/ZF/Constructible/Relative.thy
changeset 13514 cc3bbaf1b8d3
parent 13505 52a16cb7fefb
child 13535 007559e981c7
     1.1 --- a/src/ZF/Constructible/Relative.thy	Wed Aug 21 15:57:24 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Aug 22 12:28:41 2002 +0200
     1.3 @@ -253,10 +253,10 @@
     1.4      "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
     1.5  
     1.6    Union_ax :: "(i=>o) => o"
     1.7 -    "Union_ax(M) == \<forall>x[M]. (\<exists>z[M]. big_union(M,x,z))"
     1.8 +    "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
     1.9  
    1.10    power_ax :: "(i=>o) => o"
    1.11 -    "power_ax(M) == \<forall>x[M]. (\<exists>z[M]. powerset(M,x,z))"
    1.12 +    "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
    1.13  
    1.14    univalent :: "[i=>o, i, [i,i]=>o] => o"
    1.15      "univalent(M,A,P) == 
    1.16 @@ -265,17 +265,16 @@
    1.17    replacement :: "[i=>o, [i,i]=>o] => o"
    1.18      "replacement(M,P) == 
    1.19        \<forall>A[M]. univalent(M,A,P) -->
    1.20 -      (\<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)))"
    1.21 +      (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
    1.22  
    1.23    strong_replacement :: "[i=>o, [i,i]=>o] => o"
    1.24      "strong_replacement(M,P) == 
    1.25        \<forall>A[M]. univalent(M,A,P) -->
    1.26 -      (\<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))))"
    1.27 +      (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
    1.28  
    1.29    foundation_ax :: "(i=>o) => o"
    1.30      "foundation_ax(M) == 
    1.31 -	\<forall>x[M]. (\<exists>y\<in>x. M(y))
    1.32 -                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
    1.33 +	\<forall>x[M]. (\<exists>y\<in>x. M(y)) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
    1.34  
    1.35  
    1.36  subsection{*A trivial consistency proof for $V_\omega$ *}