# HG changeset patch
# User paulson
# Date 1013593447 -3600
# Node ID 3f86b73d592de6eb01a3f89aaa41dc2525443c2d
# Parent  e20f14f7ff357e66b8b390e5cfd038df73ef114a
new lemmas for closure under Union

diff -r e20f14f7ff35 -r 3f86b73d592d src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Tue Feb 12 20:35:35 2002 +0100
+++ b/src/ZF/Univ.ML	Wed Feb 13 10:44:07 2002 +0100
@@ -287,6 +287,18 @@
 by (REPEAT (ares_tac [Pair_in_VLimit] 1));
 qed "Transset_Pair_subset_VLimit";
 
+Goal "[| X: Vfrom(A,j);  Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))";
+by (dtac Transset_Vfrom 1);
+by (rtac subset_mem_Vfrom 1);
+by (rewtac Transset_def);
+by (Blast_tac 1);
+qed "Union_in_Vfrom";
+
+Goal "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)";
+by (rtac (Limit_VfromE) 1 THEN REPEAT (assume_tac 1));
+by (blast_tac (claset() addIs [Limit_has_succ, Limit_VfromI, Union_in_Vfrom]) 1); 
+qed "Union_in_VLimit";
+
 
 (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
      is a model of simple type theory provided A is a transitive set
@@ -584,6 +596,11 @@
 by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
 qed "Pair_in_univ";
 
+Goalw [univ_def]
+     "[| X: univ(A);  Transset(A) |] ==> Union(X) : univ(A)";
+by (REPEAT (ares_tac [Union_in_VLimit, Limit_nat] 1));
+qed "Union_in_univ";
+
 Goalw [univ_def] "univ(A)*univ(A) <= univ(A)";
 by (rtac (Limit_nat RS product_VLimit) 1);
 qed "product_univ";