src/ZF/Cardinal.thy

 apply (simp add: Card_def)
 apply (drule le_imp_subset)
 apply (blast elim: mem_irrefl)
 done
 
-ML
-{*
-val Least_def = @{thm Least_def};
-val eqpoll_def = @{thm eqpoll_def};
-val lepoll_def = @{thm lepoll_def};
-val lesspoll_def = @{thm lesspoll_def};
-val cardinal_def = @{thm cardinal_def};
-val Finite_def = @{thm Finite_def};
-val Card_def = @{thm Card_def};
-val eq_imp_not_mem = @{thm eq_imp_not_mem};
-val decomp_bnd_mono = @{thm decomp_bnd_mono};
-val Banach_last_equation = @{thm Banach_last_equation};
-val decomposition = @{thm decomposition};
-val schroeder_bernstein = @{thm schroeder_bernstein};
-val bij_imp_eqpoll = @{thm bij_imp_eqpoll};
-val eqpoll_refl = @{thm eqpoll_refl};
-val eqpoll_sym = @{thm eqpoll_sym};
-val eqpoll_trans = @{thm eqpoll_trans};
-val subset_imp_lepoll = @{thm subset_imp_lepoll};
-val lepoll_refl = @{thm lepoll_refl};
-val le_imp_lepoll = @{thm le_imp_lepoll};
-val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll};
-val lepoll_trans = @{thm lepoll_trans};
-val eqpollI = @{thm eqpollI};
-val eqpollE = @{thm eqpollE};
-val eqpoll_iff = @{thm eqpoll_iff};
-val lepoll_0_is_0 = @{thm lepoll_0_is_0};
-val empty_lepollI = @{thm empty_lepollI};
-val lepoll_0_iff = @{thm lepoll_0_iff};
-val Un_lepoll_Un = @{thm Un_lepoll_Un};
-val eqpoll_0_is_0 = @{thm eqpoll_0_is_0};
-val eqpoll_0_iff = @{thm eqpoll_0_iff};
-val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un};
-val lesspoll_not_refl = @{thm lesspoll_not_refl};
-val lesspoll_irrefl = @{thm lesspoll_irrefl};
-val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll};
-val lepoll_well_ord = @{thm lepoll_well_ord};
-val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll};
-val inj_not_surj_succ = @{thm inj_not_surj_succ};
-val lesspoll_trans = @{thm lesspoll_trans};
-val lesspoll_trans1 = @{thm lesspoll_trans1};
-val lesspoll_trans2 = @{thm lesspoll_trans2};
-val Least_equality = @{thm Least_equality};
-val LeastI = @{thm LeastI};
-val Least_le = @{thm Least_le};
-val less_LeastE = @{thm less_LeastE};
-val LeastI2 = @{thm LeastI2};
-val Least_0 = @{thm Least_0};
-val Ord_Least = @{thm Ord_Least};
-val Least_cong = @{thm Least_cong};
-val cardinal_cong = @{thm cardinal_cong};
-val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll};
-val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll};
-val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE};
-val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff};
-val Ord_cardinal_le = @{thm Ord_cardinal_le};
-val Card_cardinal_eq = @{thm Card_cardinal_eq};
-val CardI = @{thm CardI};
-val Card_is_Ord = @{thm Card_is_Ord};
-val Card_cardinal_le = @{thm Card_cardinal_le};
-val Ord_cardinal = @{thm Ord_cardinal};
-val Card_iff_initial = @{thm Card_iff_initial};
-val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll};
-val Card_0 = @{thm Card_0};
-val Card_Un = @{thm Card_Un};
-val Card_cardinal = @{thm Card_cardinal};
-val cardinal_mono = @{thm cardinal_mono};
-val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt};
-val Card_lt_imp_lt = @{thm Card_lt_imp_lt};
-val Card_lt_iff = @{thm Card_lt_iff};
-val Card_le_iff = @{thm Card_le_iff};
-val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le};
-val lepoll_cardinal_le = @{thm lepoll_cardinal_le};
-val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll};
-val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll};
-val cardinal_subset_Ord = @{thm cardinal_subset_Ord};
-val cons_lepoll_consD = @{thm cons_lepoll_consD};
-val cons_eqpoll_consD = @{thm cons_eqpoll_consD};
-val succ_lepoll_succD = @{thm succ_lepoll_succD};
-val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le};
-val nat_eqpoll_iff = @{thm nat_eqpoll_iff};
-val nat_into_Card = @{thm nat_into_Card};
-val cardinal_0 = @{thm cardinal_0};
-val cardinal_1 = @{thm cardinal_1};
-val succ_lepoll_natE = @{thm succ_lepoll_natE};
-val n_lesspoll_nat = @{thm n_lesspoll_nat};
-val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n};
-val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ};
-val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll};
-val lesspoll_succ_iff = @{thm lesspoll_succ_iff};
-val lepoll_succ_disj = @{thm lepoll_succ_disj};
-val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt};
-val lt_not_lepoll = @{thm lt_not_lepoll};
-val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff};
-val Card_nat = @{thm Card_nat};
-val nat_le_cardinal = @{thm nat_le_cardinal};
-val cons_lepoll_cong = @{thm cons_lepoll_cong};
-val cons_eqpoll_cong = @{thm cons_eqpoll_cong};
-val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff};
-val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff};
-val singleton_eqpoll_1 = @{thm singleton_eqpoll_1};
-val cardinal_singleton = @{thm cardinal_singleton};
-val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1};
-val succ_eqpoll_cong = @{thm succ_eqpoll_cong};
-val sum_eqpoll_cong = @{thm sum_eqpoll_cong};
-val prod_eqpoll_cong = @{thm prod_eqpoll_cong};
-val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll};
-val Diff_sing_lepoll = @{thm Diff_sing_lepoll};
-val lepoll_Diff_sing = @{thm lepoll_Diff_sing};
-val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll};
-val lepoll_1_is_sing = @{thm lepoll_1_is_sing};
-val Un_lepoll_sum = @{thm Un_lepoll_sum};
-val well_ord_Un = @{thm well_ord_Un};
-val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum};
-val Finite_0 = @{thm Finite_0};
-val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite};
-val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite};
-val lepoll_Finite = @{thm lepoll_Finite};
-val subset_Finite = @{thm subset_Finite};
-val Finite_Diff = @{thm Finite_Diff};
-val Finite_cons = @{thm Finite_cons};
-val Finite_succ = @{thm Finite_succ};
-val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord};
-val Finite_imp_well_ord = @{thm Finite_imp_well_ord};
-val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel};
-val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel};
-val well_ord_converse = @{thm well_ord_converse};
-val ordertype_eq_n = @{thm ordertype_eq_n};
-val Finite_well_ord_converse = @{thm Finite_well_ord_converse};
-val nat_into_Finite = @{thm nat_into_Finite};
-*}
-
 end