equal
deleted
inserted
replaced
69 apply (blast intro: Un_lepoll_Inf_Ord_weak) |
69 apply (blast intro: Un_lepoll_Inf_Ord_weak) |
70 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) |
70 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) |
71 apply (rule Un_upper1 [THEN subset_imp_lepoll]) |
71 apply (rule Un_upper1 [THEN subset_imp_lepoll]) |
72 done |
72 done |
73 |
73 |
74 lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)" |
74 schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)" |
75 apply (rule RepFun_bijective) |
75 apply (rule RepFun_bijective) |
76 apply (simp add: doubleton_eq_iff, blast) |
76 apply (simp add: doubleton_eq_iff, blast) |
77 done |
77 done |
78 |
78 |
79 lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x" |
79 lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x" |