equal
deleted
inserted
replaced
93 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
93 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
94 by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
94 by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
95 qed "Inf_Card_is_InfCard"; |
95 qed "Inf_Card_is_InfCard"; |
96 |
96 |
97 Goal "(THE z. {x}={z}) = x"; |
97 Goal "(THE z. {x}={z}) = x"; |
98 by (fast_tac (claset() addSIs [the_equality] |
98 by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
99 addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
|
100 qed "the_element"; |
99 qed "the_element"; |
101 |
100 |
102 Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
101 Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
103 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
102 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
104 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
103 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |