# HG changeset patch
# User paulson
# Date 862393357 -7200
# Node ID 1fba53dcbf1d3262ca28734711f0604c7073bd5c
# Parent  88366253a09af020c1e8b5b11e7a2f3b65c3760d
New theorems Pow_in_Vfrom and Pow_in_VLimit

diff -r 88366253a09a -r 1fba53dcbf1d src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Wed Apr 30 11:25:31 1997 +0200
+++ b/src/ZF/Univ.ML	Wed Apr 30 11:42:37 1997 +0200
@@ -382,6 +382,22 @@
                       limiti RS Limit_has_succ] 1));
 qed "fun_in_VLimit";
 
+goalw Univ.thy [Pi_def]
+    "!!A. [| a: Vfrom(A,j);  Transset(A) |] ==> \
+\         Pow(a) : Vfrom(A, succ(succ(j)))";
+by (dtac Transset_Vfrom 1);
+by (rtac subset_mem_Vfrom 1);
+by (rewtac Transset_def);
+by (stac Vfrom 1);
+by (Blast_tac 1);
+qed "Pow_in_Vfrom";
+
+goal Univ.thy
+  "!!a. [| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
+by (blast_tac (!claset addEs [Limit_VfromE]
+		       addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
+qed "Pow_in_VLimit";
+
 
 (*** The set Vset(i) ***)