equal
deleted
inserted
replaced
15 "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] |
15 "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] |
16 ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)" |
16 ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)" |
17 apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI) |
17 apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI) |
18 apply (rule conjI) |
18 apply (rule conjI) |
19 apply (rule_tac [2] le_UN_Ord_lt_csucc) |
19 apply (rule_tac [2] le_UN_Ord_lt_csucc) |
20 apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE) |
20 apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) |
21 apply (simp_all add: ) |
|
22 prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE) |
21 prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE) |
23 apply (rule Pi_type) |
22 apply (rule Pi_type) |
24 apply (rename_tac [2] d) |
23 apply (rename_tac [2] d) |
25 apply (erule_tac [2] fun_Limit_VfromE, simp_all) |
24 apply (erule_tac [2] fun_Limit_VfromE, simp_all) |
26 apply (subgoal_tac "f`d : Vfrom (A, LEAST i. f`d : Vfrom (A,i))") |
25 apply (subgoal_tac "f`d : Vfrom (A, LEAST i. f`d : Vfrom (A,i))") |
42 apply (rule Vfrom [THEN ssubst]) |
41 apply (rule Vfrom [THEN ssubst]) |
43 apply (drule fun_is_rel) |
42 apply (drule fun_is_rel) |
44 (*This level includes the function, and is below csucc(K)*) |
43 (*This level includes the function, and is below csucc(K)*) |
45 apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2]) |
44 apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2]) |
46 apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ |
45 apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ |
47 Un_least_lt); |
46 Un_least_lt) |
48 apply (erule subset_trans [THEN PowI]) |
47 apply (erule subset_trans [THEN PowI]) |
49 apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2) |
48 apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2) |
50 done |
49 done |
51 |
50 |
52 lemma fun_in_Vcsucc: |
51 lemma fun_in_Vcsucc: |