(* Copyright 2021 (C) Mihails Milehins *) chapter‹Set Theory for Category Theory› section‹Introduction› theory CZH_Sets_Introduction imports CZH_Introduction CZH_Sets_MIF CZH_Utilities Intro_Dest_Elim.IHOL_IDE Conditional_Simplification.IHOL_CS ZFC_in_HOL.Cantor_NF "HOL-Eisbach.Eisbach" begin subsection‹Background› text‹ This chapter presents a formalization of the elements of set theory in the object logic ‹ZFC in HOL› (\<^cite>‹"paulson_zermelo_2019"›, also see \<^cite>‹"barkaoui_partizan_2006"›) of the formal proof assistant Isabelle \<^cite>‹"paulson_natural_1986"›. The emphasis of this work is on the improvement of the convenience of the formalization of abstract mathematics internalized in the type \<^typ>‹V›. › subsection‹References, related and previous work› text‹ The results that are presented in this chapter cannot be traced to a single source of information. Nonetheless, the results are not original. A significant number of these results was carried over (with amendments) from the main library of Isabelle/HOL \<^cite>‹"noauthor_isabellehol_2020"›. Other results were inspired by elements of the content of the books ‹Introduction to Axiomatic Set Theory› by G. Takeuti and W. M. Zaring \<^cite>‹"takeuti_introduction_1971"›, ‹Theory of Sets› by N. Bourbaki \<^cite>‹"bourbaki_elements_1970"› and ‹Algebra› by T. W. Hungerford \<^cite>‹"hungerford_algebra_2003"›. Furthermore, several online encyclopedias and forums (including Wikipedia \<^cite>‹"noauthor_wikipedia_2001"›, ProofWiki \<^cite>‹"noauthor_proofwiki_nodate"›, Encyclopedia of Mathematics \<^cite>‹"noauthor_encyclopedia_nodate"›, nLab \<^cite>‹"noauthor_nlab_nodate"› and Mathematics Stack Exchange) were used consistently throughout the development of this chapter. Inspiration for the work presented in this chapter has also been drawn from a similar ongoing project in the formalization of mathematics in the system HOTG (Higher Order Tarski-Grothendieck) \<^cite>‹"brown_higher-order_2019" and "chen_hotg_2021"›. It should also be mentioned that the Isabelle/HOL and the Isabelle/ML code from the main distribution of Isabelle2020 and certain posts on the mailing list of Isabelle were frequently reused (with amendments) during the development of this chapter. Some of the specific examples of such reuse are \begin{itemize} \item The adoption of the implementation of the command @{command lemmas_with} that is available as part of the framework Types-To-Sets in the main distribution of Isabelle2020. \item The notation for the ``multiway-if'' was written by Manuel Eberl and appeared in a post on the mailing list of Isabelle: \<^cite>‹"eberl_syntax_2021"›. \end{itemize} › hide_const (open) list.set Sum subset lemmas ord_of_nat_zero = ord_of_nat.simps(1) subsection‹Notation› abbreviation (input) qm (‹(_ ? _ : _)› [0, 0, 10] 10) where "C ? A : B ≡ if C then A else B" abbreviation (input) if2 where "if2 a b ≡ (λi. (i = 0 ? a : b))" subsection‹Further foundational results› lemma theD: assumes "∃!x. P x" and "x = (THE x. P x)" shows "P x" and "P y ⟹ x = y" using assms by (metis theI)+ lemmas [intro] = bij_betw_imageI lemma bij_betwE[elim]: assumes "bij_betw f A B" and "⟦ inj_on f A; f ` A = B ⟧ ⟹ P" shows P using assms unfolding bij_betw_def by auto lemma bij_betwD[dest]: assumes "bij_betw f A B" shows "inj_on f A" and "f ` A = B" using assms by auto lemma ex1D: "∃!x. P x ⟹ P x ⟹ P y ⟹ x = y" by clarsimp text‹\newpage› end