equal
deleted
inserted
replaced
631 (*** For every cardinal number there exists a greater one |
631 (*** For every cardinal number there exists a greater one |
632 [Kunen's Theorem 10.16, which would be trivial using AC] ***) |
632 [Kunen's Theorem 10.16, which would be trivial using AC] ***) |
633 |
633 |
634 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; |
634 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; |
635 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
635 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
636 by (safe_tac (ZF_cs addSIs [Ord_ordertype])); |
636 by (fast_tac (ZF_cs addSIs [Ord_ordertype]) 2); |
637 by (rewtac Transset_def); |
637 by (rewtac Transset_def); |
638 by (safe_tac ZF_cs); |
638 by (safe_tac subset_cs); |
639 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1); |
639 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1); |
640 by (safe_tac ZF_cs); |
640 by (safe_tac ZF_cs); |
641 by (rtac UN_I 1); |
641 by (rtac UN_I 1); |
642 by (rtac ReplaceI 2); |
642 by (rtac ReplaceI 2); |
643 by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset, predE]))); |
643 by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset, predE]))); |