# HG changeset patch
# User lcp
# Date 786890293 -3600
# Node ID 06a484afc603e179a3403968a8cf84f4939d9a29
# Parent  b60e77395d1a6df826aedd3ce74ae878219c1877
Card_cardinal_le: new

diff -r b60e77395d1a -r 06a484afc603 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Dec 08 12:46:25 1994 +0100
+++ b/src/ZF/Cardinal.ML	Thu Dec 08 13:38:13 1994 +0100
@@ -169,7 +169,8 @@
 by (simp_tac (FOL_ss addsimps prems) 1);
 qed "Least_cong";
 
-(*Need AC to prove   X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le  *)
+(*Need AC to prove   X lepoll Y ==> |X| le |Y| ; 
+  see well_ord_lepoll_imp_Card_le  *)
 goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
 by (rtac Least_cong 1);
 by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
@@ -216,6 +217,10 @@
 by (rtac Ord_Least 1);
 qed "Card_is_Ord";
 
+goal Cardinal.thy "!!K. Card(K) ==> K le |K|";
+by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
+val Card_cardinal_le = result();
+
 goalw Cardinal.thy [cardinal_def] "Ord(|A|)";
 by (rtac Ord_Least 1);
 qed "Ord_cardinal";