# HG changeset patch
# User lcp
# Date 776967060 -7200
# Node ID e1de521e012af44133695c46e7972e7482ed86bd
# Parent  dfca17a698b01a8c26a11766a64dde355aa029f6
ZF/Cardinal/Card_Un: new

diff -r dfca17a698b0 -r e1de521e012a src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Mon Aug 15 18:09:37 1994 +0200
+++ b/src/ZF/Cardinal.ML	Mon Aug 15 18:11:00 1994 +0200
@@ -225,6 +225,17 @@
 by (fast_tac (ZF_cs addSEs [ltE]) 1);
 val Card_0 = result();
 
+val [premK,premL] = goal Cardinal.thy
+    "[| Card(K);  Card(L) |] ==> Card(K Un L)";
+by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1);
+by (asm_simp_tac 
+    (ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1);
+by (asm_simp_tac
+    (ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1);
+val Card_Un = result();
+
+(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
+
 goalw Cardinal.thy [cardinal_def] "Card(|A|)";
 by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
 by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);