equal
deleted
inserted
replaced
55 well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 |
55 well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 |
56 THEN REPEAT (assume_tac 1)); |
56 THEN REPEAT (assume_tac 1)); |
57 qed "Un_eqpoll_Inf_Ord"; |
57 qed "Un_eqpoll_Inf_Ord"; |
58 |
58 |
59 |
59 |
60 (*bijection is inferred!*) |
60 Goal "?f : bij({{y,z}. y:x}, x)"; |
61 Goal "(lam u:{{y,z} . y: x}. THE y. {y,z} = u) : bij({{y,z}. y:x}, x)"; |
|
62 by (rtac RepFun_bijective 1); |
61 by (rtac RepFun_bijective 1); |
63 by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1); |
62 by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1); |
64 by (Blast_tac 1); |
63 by (Blast_tac 1); |
65 qed "paired_bij"; |
64 qed "paired_bij"; |
66 |
65 |