equal
deleted
inserted
replaced
438 ==> \<exists>c<a. h`y \<subseteq> f`c & |
438 ==> \<exists>c<a. h`y \<subseteq> f`c & |
439 (\<forall>b<a. h`b \<subseteq> f`c --> |
439 (\<forall>b<a. h`b \<subseteq> f`c --> |
440 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))" |
440 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))" |
441 apply (drule ex_next_set, assumption+) |
441 apply (drule ex_next_set, assumption+) |
442 apply (erule bexE) |
442 apply (erule bexE) |
443 apply (rule oexI) |
443 apply (rule_tac x="converse(f)`X" in oexI) |
444 apply (subst right_inverse_bij, blast, assumption+) |
444 apply (simp add: right_inverse_bij) |
445 apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI |
445 apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI |
446 Card_is_Ord) |
446 Card_is_Ord) |
447 done |
447 done |
448 |
448 |
449 |
449 |