15 (* ********************************************************************** *) |
15 (* ********************************************************************** *) |
16 (* AC1 ==> AC18 *) |
16 (* AC1 ==> AC18 *) |
17 (* ********************************************************************** *) |
17 (* ********************************************************************** *) |
18 |
18 |
19 lemma PROD_subsets: |
19 lemma PROD_subsets: |
20 "[| f \<in> (\<Pi>b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |] |
20 "[| f \<in> (\<Pi> b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |] |
21 ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi>a \<in> A. Q(a))" |
21 ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi> a \<in> A. Q(a))" |
22 by (rule lam_type, drule apply_type, auto) |
22 by (rule lam_type, drule apply_type, auto) |
23 |
23 |
24 lemma lemma_AC18: |
24 lemma lemma_AC18: |
25 "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X)); A \<noteq> 0 |] |
25 "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |] |
26 ==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> |
26 ==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> |
27 (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))" |
27 (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))" |
28 apply (rule subsetI) |
28 apply (rule subsetI) |
29 apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE) |
29 apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE) |
30 apply (erule impE, fast) |
30 apply (erule impE, fast) |
31 apply (erule exE) |
31 apply (erule exE) |
32 apply (rule UN_I) |
32 apply (rule UN_I) |
65 apply (rule subst_elem, assumption) |
65 apply (rule subst_elem, assumption) |
66 apply (fast elim: notE subst_elem) |
66 apply (fast elim: notE subst_elem) |
67 done |
67 done |
68 |
68 |
69 lemma lemma1_2: |
69 lemma lemma1_2: |
70 "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B); a \<in> A |] |
70 "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B); a \<in> A |] |
71 ==> f`(uu(a))-{0} \<in> a" |
71 ==> f`(uu(a))-{0} \<in> a" |
72 apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type) |
72 apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type) |
73 done |
73 done |
74 |
74 |
75 lemma lemma1: "\<exists>f. f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi>B \<in> A. B)" |
75 lemma lemma1: "\<exists>f. f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi> B \<in> A. B)" |
76 apply (erule exE) |
76 apply (erule exE) |
77 apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})" |
77 apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})" |
78 in exI) |
78 in exI) |
79 apply (rule lam_type) |
79 apply (rule lam_type) |
80 apply (simp add: lemma1_2) |
80 apply (simp add: lemma1_2) |