equal
deleted
inserted
replaced
36 by (Blast_tac 1); |
36 by (Blast_tac 1); |
37 qed "inj_PiBij"; |
37 qed "inj_PiBij"; |
38 |
38 |
39 |
39 |
40 |
40 |
41 Goal "PiBij A B `` (Pi A B) = Graph A B"; |
41 Goal "PiBij A B ` (Pi A B) = Graph A B"; |
42 by (rtac equalityI 1); |
42 by (rtac equalityI 1); |
43 by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1); |
43 by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1); |
44 by (rtac subsetI 1); |
44 by (rtac subsetI 1); |
45 by (asm_full_simp_tac (simpset() addsimps [image_def]) 1); |
45 by (asm_full_simp_tac (simpset() addsimps [image_def]) 1); |
46 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1); |
46 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1); |