equal
deleted
inserted
replaced
31 qed "WO1_WO2"; |
31 qed "WO1_WO2"; |
32 |
32 |
33 (* ********************************************************************** *) |
33 (* ********************************************************************** *) |
34 |
34 |
35 goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
35 goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
36 by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1); |
36 by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1); |
37 val lam_sets = result(); |
37 val lam_sets = result(); |
38 |
38 |
39 goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
39 goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
40 by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1); |
40 by (fast_tac (ZF_cs addSIs [equalityI] addSEs [apply_type]) 1); |
41 val surj_imp_eq_ = result(); |
41 val surj_imp_eq_ = result(); |
42 |
42 |
43 goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
43 goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
44 by (fast_tac (AC_cs addSDs [surj_imp_eq_] |
44 by (fast_tac (AC_cs addSDs [surj_imp_eq_] |
45 addSIs [equalityI, ltI] addSEs [ltE]) 1); |
45 addSIs [equalityI, ltI] addSEs [ltE]) 1); |