11 (* - Sigma_fun_space_not0 *) |
11 (* - Sigma_fun_space_not0 *) |
12 (* - all_eqpoll_imp_pair_eqpoll *) |
12 (* - all_eqpoll_imp_pair_eqpoll *) |
13 (* - Sigma_fun_space_eqpoll *) |
13 (* - Sigma_fun_space_eqpoll *) |
14 (* ********************************************************************** *) |
14 (* ********************************************************************** *) |
15 |
15 |
16 goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C"; |
|
17 by (Fast_tac 1); |
|
18 qed "mem_not_eq_not_mem"; |
|
19 |
|
20 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0"; |
16 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0"; |
21 by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1] |
17 by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, |
22 addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1); |
18 Union_empty_iff RS iffD1] |
|
19 addDs [fun_space_emptyD]) 1); |
23 qed "Sigma_fun_space_not0"; |
20 qed "Sigma_fun_space_not0"; |
24 |
21 |
25 Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)"; |
22 Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)"; |
26 by (REPEAT (rtac ballI 1)); |
23 by (REPEAT (rtac ballI 1)); |
27 by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1 |
24 by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1 |