%(* \documentclass[12pt]{article} \newcommand{\invisible}[1]{} \newcommand{\verba}[1]{+#1+} \begin{document} \section*{An experiment in writing formal mathematics in Coq} \noindent Carlos Simpson\newline carlos@math.unice.fr\newline CNRS, Laboratoire J.A. Dieudonne\newline Universite de Nice-Sophia Antipolis \begin{center} {\bf Introduction} \end{center} We present here a small attempt at writing proofs in a formal language. Many different efforts in this direction have been going on for quite some time. For example the {\em Journal of Formalized Mathematics} has been publishing articles verified in the MIZAR system since at least 1989. What we do here is by no means as much as what has been done in the MIZAR system \cite{Mizar}, the HOL system \cite{HOL}, the Isabelle system \cite{Isabelle}, or in Coq \cite{Coq}; and indeed most of what we do is contained in a Coq contribution dating from 1995. Nonetheless, it still seems necessary to do some work toward developing a mathematical style which would be convenient and easy to use for the ordinary mathematician. We try to make a contribution in this direction by presenting a proof development wherein the definitions and proofs are written in a style which is precise yet easy to understand. The reader will judge whether this has been successful. We start from an axiomatization of set theory which is close to what Benjamin Werner constructed \cite{Werner}. I suppose that if you replace our parameter Ens by the Ens which he constructed, then one should be able to prove the things which we suppose as axioms, relatively easily from his paper. However, we don't treat that here, rather we just start with some reasonable-sounding axioms. Then we proceed with the standard development of ZFC set theory. Our definition of pair is slightly different from the standard one, designed to make the proofs of the main lemmas about pairs a little easier and more transparent. Our goal is to introduce functions and prove some basic properties. We also introduce the set Naturals and prove some basic properties. See below for a summary of parameters, axioms, definitions and theorems (only after this summary does the actual Coq file start). Most of what we do was already done by Guillaume Alexandre in his Coq contribution ``An axiomatisation of intuitionistic Zermelo-Fraenkel set theory'' (zf, 1995) \cite{Alexandre}, indeed we start with the same parameters and similar axioms. We use classical logic (which is easier) though: our parameter Ens is in Type. It is also worth noting that everything we do here is also already known in the context of the MIZAR system \cite{Mizar}. It also seems to have been done (again in a much more complete way) in the ``ZF'' logic in the Isabelle system \cite{Isabelle}. Thus it is extremely unlikely that there is anything new in the present work. Rather, our purpose is twofold: first, to create some publicity for all of these efforts, basically by showing that anybody with a solid knowledge of mathematical foundations can begin to write mathematics in a theorem-proving system; and second to suggest a style of writing that might allow for ease of further advancement toward the ultimate goal of writing modern high-level research mathematics in a theorem-proving environment. For example, the main difference between the present work and Alexandre's file \cite{Alexandre} is in the writing style: we don't use the Coq proof engine but rather construct explicitly the proof terms, depending often on the Section mechanism. The file compiles in about 6 seconds using the native code version 6.2.3 on our Linux server. This style of proof development can be thought of as an attempt to implement some of the ideas discussed in the TPHOLs '99 volume (for example the article by Markus Wenzel about Isar \cite{Wenzel}). Our functions \verb}CHOICE} and \verb}REPLACEMENT} are defined on all properties \verb}P: Ens ->Prop}; however they satisfy the required properties \verb}CHOICE_pr} and \verb}REPLACEMENT_pr1}, \verb}REPLACEMENT_pr2}, only when \verb}P} holds for one element (in the case of \verb}CHOICE}) or when \verb}P} is bounded (in the case of \verb}REPLACEMENT}). Since all other constructions are based on these (plus a few everywhere-defined constructions in the parameters) we gain the beneficial situation that all of our constructions are defined as \verb}Ens->Ens}; no constructions depend on proofs. This can be contrasted with the ``setoid'' approach. Our constructions have the required properties only when the arguments have the required properties. Thus for example we have a construction \verb}(EV f x)} defined for all sets \verb}f} and \verb}x}: however, it represents what one might call the evaluation of the function f on the element x, only when \verb}(IN x (Domain f))}. The system of axioms which we assume was just invented on the spur of the moment; it is basically ZFC but there are probably several redundancies. Also there is a certain interaction between this ZFC and the ambient type-theoretic language of Coq, which seems to mean that we are probably implicitly assuming the existence of one or maybe two inaccessible cardinals. See Werner's paper ``Sets in Types, Types in Sets'' for the discussion that underlies our justification for doing what we are doing. A possible perspective of the present work is that one could envision coding this first half of Werner's paper, giving a construction Type -> Ens with the properties he describes. This might be useful. \begin{center} {\bf A short course in Coq} \end{center} This section is addressed to readers who are unfamiliar with type-theoretical theorem proving systems (as I was until a few months ago). We try to explain rapidly the basic elements of how to write classical mathematics according to one interpretation of things. This information was obtained from two sources: Andr\'e Hirschowitz whom I warmly thank for explaining much of the basics; and the Coq system reference manual \cite{Coq-ref}. The present explanation is of course redundant with respect to \cite{Coq-ref}; however it might be useful because we concentrate on those aspects of Coq which we actually use. Names of objects are strings of letters and numerals and the symbol \verb+_+ which takes the place of a space; actual spaces have meaning (they separate different objects). All lines begin with a capitalized command and end with a period. \verb}Parameter} means we introduced something. \verb}Definition} means we give a definition. All objects are ``terms''. Some terms are also ``Types''. When a term is a type, it can have member terms. If \verb}A} is a term of type \verb}B} we write \verb}A:B}. A particular term is \verb}Prop}. It is a type whose members are themselves types known as ``propositions''. If \verb}P} is a proposition (written \verb}P : Prop} ) then a term \verb}p} of type \verb}P} (written \verb}p:P}) denotes a ``proof'' of the proposition \verb}P}. If \verb}A} and \verb}B} are types then there is a type denoted \verb}A -> B}. The terms of type \verb}A -> B} are functions from \verb}A} to \verb}B}; and they can be applied to terms of type \verb}A} to obtain terms of type \verb}B}. Application is written as juxtaposition separated by a space and delimited by parenthesis. Thus if \verb}f: A-> B} and if \verb}a: A} then \verb}(f a) : B}. We work with the type \verb}Prop}, and with one other type which we introduce in the first line of the file, called \verb}Ens}. The member terms of \verb}Ens} are thought of as ``sets''. However, an \verb}X: Ens} is not itself a type. Its member elements are other \verb}Y: Ens} which satisfy the property \verb}(IN Y X)} which we introduce in the second line of the file. The method described in the above paragraph has already been used by Guillaume Alexandre \cite{Alexandre}. The main symbols which are used are parentheses and square brackets. Parentheses are sometimes used to delimit expressions in the usual way. The other use is to write the statement ``for all''. Suppose \verb}P} is a property on \verb}Ens}, i.e. \verb}P: Ens-> Prop}. This could be coded by saying \begin{verbatim} Parameter P : Ens-> Prop. \end{verbatim} or if we are in a section, equivalently \begin{verbatim} Variable P : Ens -> Prop. \end{verbatim} Then the statement ``for all X in Ens, P of X'' is written: \begin{verbatim} Definition example1 : Prop := (X: Ens)(P X). \end{verbatim} This line of code actually says that we define a new object, which is a term of type Prop (i.e. a proposition), which says that for all \verb}X: Ens, (P X)}. Square brackets mean ``maps to''. Thus we could write \begin{verbatim} Definition example2 : Ens -> Prop := [X: Ens] (P X). \end{verbatim} In this example, example2 is actually equal to P and in fact Coq treats them as interchangeable. A slightly more nontrivial example would be the ``constant property'': \begin{verbatim} Parameter Q : Prop. Definition example3 : Ens-> Prop := [X: Ens] Q. \end{verbatim} This object is of type \verb}Ens-> Prop}. If \verb}Y: Ens} then the value \verb}(example3 Y)} is equal to \verb}Q} (i.e. interchangeable with \verb}Q} by Coq). Functions of several variables : if \verb}A},\verb}B} and \verb}C} are types then a term \verb}f: A-> B-> C} means a term of type \verb}A-> (B -> C)}; these parentheses can be omitted. If \verb}f} is such a term and if \verb}a: A} and \verb}b: B} then \verb}(f a)} is of type \verb}(B-> C)}, so we can form \verb}((f a) b)} which is of type \verb}C}. Again the inner parentheses can be omitted and this can be written as \verb}(f a b)}. Caution : statements like \verb}(a:A)} are not themselves propositions, i.e. we cannot write \verb}(a:A):Prop}. This is the basic reason why we treat sets which are just terms and not types, and we introduce a separate inclusion relation for sets denoted \verb}(IN X Y)}. If \verb}X: Ens} and \verb}Y: Ens} then \verb}(IN X Y) : Prop}. If \verb}P: Prop} then we can issue the statement \begin{verbatim} Axiom axiom1 : P. \end{verbatim} This introduces a term denoted axiom1 which is a proof of \verb}P}. One can note that proofs and other terms are manipulated by exactly the same symbols \verb}(a:A)} and \verb}[a:A]}. If \verb}P} is a proposition then \verb}(p:P) Q} means \verb}P} implies \verb}Q} ; if \verb}Q} doesn't depend on \verb}p} then it can also be written \verb}P -> Q}. For other types \verb}A,B}, the phrase \verb}(a:A) B} means the type of functions which to \verb}a:A} associate a term of type \verb}B}. If \verb}B} is independent of \verb}a} then this is equivalent to the type \verb}A-> B} (they are two ways of writing the same thing i.e. interchangeable for Coq). On the other hand, \verb}B} could be a complex formula which depends on \verb}a:A}. In this case, \verb}(a:A) B} is the type, whose member terms are ``sections'' associating to each a a term of type ``B of a''. This is best understood when it arises in practice. If one issues the statement \begin{verbatim} Theorem theorem1 : P. \end{verbatim} this means that we claim a theorem whose proof is denoted theorem1, of type \verb}P} i.e. \verb}theorem1} is a proof of proposition \verb}P}. This statement should be followed by a ``proof'' which can have many forms in the full version of Coq. In the very restricted part of Coq which we use here, all proofs are written as \begin{verbatim} Proof p. \end{verbatim} where \verb}p} is an already-existing term (which could be a new composite of old terms) of type \verb}P}. Once this is done, the fact that there is a proof named \verb}theorem1}, of the proposition \verb}P}, is remembered but the structure of the old proof \verb}p} is forgotten (this is called ``proof irrelevance''). This is good because it prevents the machine from getting bogged down by remembering long proofs. The last piece of machinery which needs to be explained is the notion of section. A section is started with the command \begin{verbatim} Section section_name. \end{verbatim} and ended with the command \begin{verbatim} End section_name. \end{verbatim} Within a section, one can introduce local variables (i.e. variables which are forgotten when the section is closed) with the command \begin{verbatim} Variable X : A. \end{verbatim} which introduces a term \verb}X} of type \verb}A}; the phrase \begin{verbatim} Hypothesis p: P. \end{verbatim} is equivalent to \verb}Variable p: P.} and is (by convention) used when \verb}P} is a proposition. The command \begin{verbatim} Local A:= B. \end{verbatim} defines a local variable denoted \verb}A} (a redefinition of \verb}B}). This is contrasted with \verb}Definition} which, when used in a section, defines a global object which is remembered after the section. The command \begin{verbatim} Remark step1 : P. \end{verbatim} is the same as \verb}Theorem} but it is local; it has to be followed by \verb}Proof ... .} and, fortunately, its name will be forgotten when the section is closed. This allows us to use the names \verb}step1}, \verb}step2}, etc. in every section. The command \begin{verbatim} Fact step1 : P. \end{verbatim} is like \verb}Remark} or \verb}Theorem} but it is semi-local, it persists in the next higher section but is then forgotten. The command \verb}Lemma} is equivalent to \verb}Theorem} (not local). These have to have unique names because their names cannot be reused. A section will typically close with a \verb}Lemma}; then right after the section is closed, the \verb}Lemma} is redefined as a \verb}Theorem}. The theorem takes into account the local variables which were defined in the section. (in reality, Coq remembers the lemma but changes its meaning to take into account the local variables; it is convenient to rewrite this as a theorem so that the new meaning is visible to the user). This is all best understood when it comes up in the file. A simple example would be to redefine our example example2 from above: \begin{verbatim} Parameter P: Ens-> Prop. Section example2_section. Variable X : Ens. Definition example2bis := (P X). End example2_section. Definition example2ter : Ens-> Prop := example2bis. \end{verbatim} \begin{center} {\em Advanced remark} \end{center} A feature which is sometimes annoying and sometimes useful is that a \verb}Lemma} or other global object defined in a section, does not necessarily ``depend'' on all of the \verb}Variables} which were introduced in the section, but only on the \verb}Variables} which actually go into its definition. For example, one CANNOT define the constant proposition of \verb}example3} above by the command \begin{verbatim} Parameter Q : Prop. Section example3_section. Variable X: Ens. Definition example3bis := Q. End example3_section. Definition example3ter : Ens->Prop := example3bis. \end{verbatim} This last line generates an error: \verb}example3bis} is of type \verb}Prop} not of type \verb}Ens-> Prop} because the variable \verb}X} was not effectively used in the definition of \verb}example3bis} inside the section. This behavior can occasionally be used to good effect, for example to define several global objects within the same section; and at other times it requires that we define constant objects by hand. \begin{center} {\em Record types} \end{center} The Coq language provides very sophisticated techniques for defining types by inductive definitions. We don't use these techniques here; however there is a special case which we use, the case of ``Record'' types. We use this in a limited case, to represent conjugation of propositions. Suppose we have several properties \begin{verbatim} Parameter P_1 : Ens -> Prop. Parameter P_2 : Ens -> Prop. Parameter P_3 : Ens -> Prop. \end{verbatim} If we want to define the property ``\verb}P_1} and \verb}P_2} and \verb}P_3}'', a conveniant approach is to use the following command: \begin{verbatim} Record ourconjugate [X: Ens] : Prop := { conjugate_1 : (P_1 X); conjugate_2 : (P_2 X); conjugate_3 : (P_3 X) }. \end{verbatim} This is read as saying that the property \verb}(ourconjugate X)} is defined as the logical and of the properties \verb}(P_1 X)}, \verb}(P_2 X)}, and \verb}(P_3 X)}. This has the effect of introducing five new objects denoted \verb}ourconjugate}, \verb}conjugate1}, \verb}conjugate2}, \verb}conjugate3} and \verb}Build_ourconjugate}. (The names \verb}ourconjugate} and \verb}conjugate_1} etc. are of course arbitrary; the system takes the assigned name \verb}ourconjugate} and adds the prefix \verb}Build_} to obtain the fifth object.) The first object is a property \verb}ourconjugate : Ens -> Prop}. The best way to illustrate how the remaining objects work is by example: suppose we have \verb}X: Ens} and suppose we have lemmas \verb}p1 : (P_1 X)}, \verb}p2 : (P_2 X)}, and \verb}p3 : (P_3 X)}. Then \begin{verbatim} (Build_ourconjugate X p1 p2 p3) \end{verbatim} is a term of type \verb}(ourconjugate X)}, thus we can write \begin{verbatim} Theorem example4 : (ourconjugate X). Proof (Build_ourconjugate X p1 p2 p3). \end{verbatim} On the other hand, suppose we know \verb}c: (ourconjugate X)}. Then we obtain terms \verb}(conjugate_1 X c) : (P_1 X)} etc., so we can write for example \begin{verbatim} Theorem example5 : (P_3 X). Proof (conjugate_3 X c). \end{verbatim} All in all, the \verb}Record} construction, used in the limited way we do here, is just a replacement for successively applying ``and''. It seems to be more natural and gives a better guide to the proof development; specially when there are 3 or more terms there is no question about parenthetisation of the iterated ``and''s; so we adopt the ``Record'' point of view rather than using ``and''. \begin{center} {\em Instructions} \end{center} To be totally explicit, here are instructions for compiling the present file. The first thing to do is to get the Coq system installed on your computer; see the website \cite{Coq}. This generates, in particular, two programs named ``coqc'' (batch-compiler) and ``coqtop'' (interactive top-level). The batch-compiler will compile any file named ``filename.v'' and tries to create the output file ``filename.vo'', giving applicable error messages when it stops. The same effect can be had in the coqtop shell by typing ``Compile Module filename.'' One could also type ``Load filename''; this gives the error messages but not the output file ``filename.vo''. The ``coqtop'' shell is an interactive shell where the user can use ``tactics'' to interactively prove theorems. This is useful for testing things out; refer to \cite{Coq-ref} for details. To get the applicable file out of the present paper, copy the \verb}.tex} source file to a ``filename.v''. There are two options: look for the line \begin{verbatim} (********* the actual Coq file starts here &&&******) \end{verbatim} below in the source file, which is where the file starts. It is hidden from Tex by an \verb+\invisible{ }+ command. (The full summary of axioms and theorems is put in between the \verb+\invisible{ }+ command and the start of the actual Coq file.) The last line of the file is designed to be a comment for Coq. Another option is to simply remove the first character of the \verb}.tex} file; then the whole discussion which you are currently reading is a comment, thus invisible, to Coq. \begin{center} {\bf Extended example} \end{center} Here we extract from the full file, some first examples of axioms and a couple of theorems, to give an idea of how things work. The reader should then look directly at the main file which is attached at the end of the \verb+.tex+ source file. \begin{verbatim} Parameter Ens : Type. Parameter IN : Ens -> Ens -> Prop. Definition SUB := [A,B: Ens] (C: Ens) ((IN C A) -> (IN C B)). Record EQ [A: Ens; B: Ens] : Prop := { EQ_forwards : (SUB A B); EQ_backwards : (SUB B A) }. (*** the following is a system theorem which we import ***) Theorem false_implies_everything : (P : Prop) (False -> P). Proof False_ind. Definition DOESNT_EXIST := [P: Ens -> Prop] ((A : Ens)(not (P A))). Definition EXISTS := [P : Ens -> Prop] (not (DOESNT_EXIST P)). Parameter EmptySet : Ens. Axiom EmptySet_pr : (DOESNT_EXIST ([X : Ens] (IN X EmptySet))). Section EXISTS_th1_proof. Variable P: Ens -> Prop. Variable X : Ens. Hypothesis p: (P X). Hypothesis h : (DOESNT_EXIST P). Remark step1 : (not (P X)). Proof (h X). Lemma EXISTS_th1_proof_Out : False. Proof (step1 p). End EXISTS_th1_proof. Theorem EXISTS_th1 : (P : Ens -> Prop) (X : Ens ) (p : (P X)) (EXISTS P) . Proof EXISTS_th1_proof_Out. Section subset_reflexive. Variable A:Ens. Variable B:Ens. Hypothesis h:(IN B A). Lemma subset_reflexive_Out : (IN B A). Proof h. End subset_reflexive. Theorem SUB_refl : (A:Ens) (SUB A A) . Proof subset_reflexive_Out. Section equality_reflexive. Variable A:Ens. Remark step1 : (SUB A A). Proof (SUB_refl A). Lemma equality_reflexive_Out : (EQ A A). Proof (Build_EQ A A step1 step1). End equality_reflexive. Theorem EQ_refl : (A:Ens) (EQ A A). Proof equality_reflexive_Out. Section equality_symmetric. Variable A:Ens. Variable B:Ens. Hypothesis h: (EQ A B). Remark stepfor : (SUB A B). Proof (EQ_forwards A B h). Remark stepback : (SUB B A). Proof (EQ_backwards A B h). Lemma equality_symmetric_Out : (EQ B A). Proof (Build_EQ B A stepback stepfor). End equality_symmetric. Theorem EQ_symm : (A,B: Ens) (EQ A B) -> (EQ B A). Proof equality_symmetric_Out. Section SUB_trans_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Hypothesis h: (SUB A B). Hypothesis k : (SUB B C). Variable X : Ens. Hypothesis m: (IN X A). Remark step1 : (IN X B). Proof (h X m). Lemma SUB_trans_proof_Out : (IN X C). Proof (k X step1). End SUB_trans_proof. Theorem SUB_trans : (A,B,C: Ens) (h:(SUB A B)) (k: (SUB B C)) (SUB A C). Proof SUB_trans_proof_Out. Section EQ_trans_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Hypothesis h: (EQ A B). Hypothesis k : (EQ B C). Remark step1 : (SUB A B). Proof (EQ_forwards A B h). Remark step2 : (SUB B A). Proof (EQ_backwards A B h). Remark step3 : (SUB B C). Proof (EQ_forwards B C k). Remark step4 : (SUB C B). Proof (EQ_backwards B C k). Remark step5 : (SUB A C). Proof (SUB_trans A B C step1 step3). Remark step6 : (SUB C A). Proof (SUB_trans C B A step4 step2). Lemma EQ_trans_proof_Out :(EQ A C). Proof (Build_EQ A C step5 step6). End EQ_trans_proof. Theorem EQ_trans: (A,B,C: Ens) (h: (EQ A B)) (k: (EQ B C)) (EQ A C). Proof EQ_trans_proof_Out. Section emptyset_empty. Variable X: Ens. Hypothesis h : (IN X EmptySet). Lemma emptyset_empty_Out : False. Proof (EmptySet_pr X h). End emptyset_empty. Theorem EmptySet_th1 : (X: Ens) (h: (IN X EmptySet)) False . Proof emptyset_empty_Out. Section emptyset_subset_everything. Variable A: Ens. Section emptyset_subset_everything_2. Variable B: Ens. Hypothesis h: (IN B EmptySet). Remark step1 : False . Proof (EmptySet_th1 B h). Lemma emptyset_subset_everything_2_Out : (IN B A) . Proof (false_implies_everything (IN B A) step1). End emptyset_subset_everything_2. Remark step2 : (B: Ens) (h: (IN B EmptySet)) (IN B A) . Proof emptyset_subset_everything_2_Out. Lemma emptyset_subset_everything_Out : (SUB EmptySet A). Proof step2. End emptyset_subset_everything. Theorem EmptySet_th2 : (A : Ens) (SUB EmptySet A) . Proof emptyset_subset_everything_Out. Definition Its_empty := [A : Ens] (X : Ens) (not (IN X A) ). Section its_empty_implies_equals_emptyset_proof. Variable A: Ens. Hypothesis k: (Its_empty A). Section ieieep1. Variable X: Ens. Hypothesis i: (IN X A). Remark step1_1 : False . Proof (k X i). Lemma ieieep1_Out : (IN X EmptySet). Proof (false_implies_everything (IN X EmptySet) step1_1). End ieieep1. Remark step1 : (SUB A EmptySet). Proof ieieep1_Out. Section ieieep2. Variable X: Ens. Hypothesis i: (IN X EmptySet). Remark step2_1 : False. Proof (EmptySet_th1 X i). Lemma ieieep2_Out : (IN X A). Proof (false_implies_everything (IN X A) step2_1). End ieieep2. Remark step2 : (SUB EmptySet A). Proof ieieep2_Out. Lemma ieieep_Out :(EQ A EmptySet). Proof (Build_EQ A EmptySet step1 step2). End its_empty_implies_equals_emptyset_proof. Theorem its_empty_implies_equals_emptyset : (A: Ens) (k: (Its_empty A)) (EQ A EmptySet). Proof ieieep_Out. Theorem Its_empty_emptyset : (Its_empty EmptySet). Proof EmptySet_th1. Definition Its_nonempty := [A : Ens] (not (Its_empty A)). Section Its_nonempty_proof. Variable X : Ens. Variable A : Ens. Hypothesis h : (IN X A). Hypothesis h2 : (Its_empty A). Lemma Its_nonempty_proof_Out : False. Proof (h2 X h). End Its_nonempty_proof. Theorem Its_nonempty_th1 : (X,A: Ens) (h : (IN X A)) (Its_nonempty A). Proof Its_nonempty_proof_Out. \end{verbatim} \begin{center} {\bf Summary} \end{center} We now give a listing of all of the parameters and axioms, most of the definitions, and some of the theorems. This summary was generated by a simple c program from the Coq source file, then pruned by hand. The Coq source file itself is viewable only in the .tex source file; this is because it is somewhat long and is not best viewed printed out in postscript. For those who insist on having a paper version, directly printing that part of the source file will be more efficient than the ``verbatim'' tex command. In case that might be useful, we have included the {\em full} summary in the source file, just before the beginning of the full Coq file. \begin{verbatim} Parameter Ens : Type . Parameter IN : Ens -> Ens -> Prop . Definition SUB := [A, B : Ens] (C : Ens) ((IN C A) -> (IN C B)). Record EQ [A : Ens ; B : Ens] : Prop := { EQ_forwards : (SUB A B); EQ_backwards : (SUB B A) }. Axiom excluded_middle : (P : Prop) (not (not P)) -> P . Theorem false_implies_everything : (P : Prop) (False -> P) . Definition DOESNT_EXIST := [P : Ens -> Prop] ((A : Ens) (not (P A))). Definition EXISTS := [P : Ens -> Prop] (not (DOESNT_EXIST P)). Parameter CHOICE : (P : Ens -> Prop) Ens . Axiom CHOICE_pr : (P : Ens -> Prop) (h : (EXISTS P)) (P (CHOICE P)) . Parameter EmptySet : Ens . Axiom EmptySet_pr : (DOESNT_EXIST ([X : Ens] (IN X EmptySet))) . Definition Bounded_By := [A : Ens] [P : Ens -> Prop] (X : Ens) ((P X) -> (IN X A)). Definition Bounded := [P : Ens -> Prop] (EXISTS ([A : Ens] (Bounded_By A P))). Parameter union : (A, B : Ens) Ens . Axiom union_pr1 : (A, B : Ens) (SUB A (union A B)) . Axiom union_pr2 : (A, B : Ens) (SUB B (union A B)) . Axiom union_pr3 : (A, B, C : Ens) (h : (SUB A C)) (k : (SUB B C)) (SUB (union A B) C) . Record nested_IN [A, B, C : Ens] : Prop := { nested_IN_ab : (IN A B); nested_IN_bc : (IN B C) }. Definition b_in_Union_a := [A, B : Ens] (EXISTS ([C : Ens] (nested_IN B C A))). Axiom Union_bounded : (F : Ens) (Bounded (b_in_Union_a F)) . Parameter Singleton : Ens -> Ens . Axiom Singleton_pr1 : (X : Ens) (IN X (Singleton X)) . Axiom Singleton_pr2 : (X : Ens) (Y : Ens) (h : (IN Y (Singleton X))) (EQ X Y) . Axiom Extensionality : (X, Y, Z : Ens) (h : (EQ X Y)) (k : (IN Y Z)) (IN X Z) . Axiom Powerset_bounded : (X : Ens) (Bounded ([Y : Ens] (SUB Y X))) . Parameter REPLACEMENT : (P : Ens -> Prop) Ens . Axiom REPLACEMENT_pr1 : (P : Ens -> Prop) (b : (Bounded P)) (X : Ens) ((P X) -> (IN X (REPLACEMENT P))) . Axiom REPLACEMENT_pr2 : (P : Ens -> Prop) (b : (Bounded P)) (X : Ens) ((IN X (REPLACEMENT P)) -> (P X)) . Definition Zero := EmptySet. Definition Next : Ens -> Ens := [X : Ens] (union X (Singleton X)). Record Contains_NN [X : Ens] : Prop := { Contains_NN_zero : (IN Zero X); Contains_NN_nexts : (A : Ens)(h : (IN A X))(IN (Next A) X) }. Axiom Infinity_exists : (EXISTS Contains_NN) . (****** the axioms are now finished ********) Theorem EXISTS_th1 : (P : Ens -> Prop) (X : Ens) (p : (P X)) (EXISTS P) . Theorem SUB_refl : (A : Ens) (SUB A A) . Theorem EQ_refl : (A : Ens) (EQ A A) . Theorem EQ_symm : (A, B : Ens) (EQ A B) -> (EQ B A) . Definition NEQ := [A, B : Ens] (not (EQ A B)). Theorem NEQ_symm : (A, B : Ens) (k : (NEQ A B)) (NEQ B A) . Theorem SUB_trans : (A, B, C : Ens) (h : (SUB A B)) (k : (SUB B C)) (SUB A C) . Theorem EQ_trans : (A, B, C : Ens) (h : (EQ A B)) (k : (EQ B C)) (EQ A C) . Record StrictSUB [A, B : Ens] : Prop := { StrictSUB_sub : (SUB A B); StrictSUB_neq : (not (EQ A B)) }. Theorem EmptySet_th1 : (X : Ens) (h : (IN X EmptySet)) False . Theorem EmptySet_th2 : (A : Ens) (SUB EmptySet A) . Definition Its_empty := [A : Ens] (X : Ens) (not (IN X A)). Definition Its_nonempty := [A : Ens] (not (Its_empty A)). Theorem Its_nonempty_th1 : (X, A : Ens) (h : (IN X A)) (Its_nonempty A) . Theorem Nothing_strictsub_Zero : (X : Ens) (not (StrictSUB X Zero)) . Theorem Bounded_th1 : (P : Ens -> Prop) (A : Ens) (h : (X : Ens) ((P X) -> (IN X A))) (Bounded P) . Theorem Bounded_th2 : (P : Ens -> Prop) (A : Ens) (h : (Bounded_By A P)) (Bounded P) . Record Restriction [P : Ens -> Prop; A, X : Ens] : Prop := { remaining_property : (P X); the_restriction : (IN X A) }. Theorem Restriction_bounded : (P : Ens -> Prop) (A : Ens) (Bounded (Restriction P A)) . Definition Set_Of := [A : Ens] [P : Ens -> Prop] (REPLACEMENT (Restriction P A)). Theorem Set_Of_th1 : (A : Ens) (P : Ens -> Prop) (X : Ens) (h : (IN X A)) (k : (P X)) (IN X (Set_Of A P)) . Theorem Set_Of_th2 : (A : Ens) (P : Ens -> Prop) (X : Ens) (h : (IN X (Set_Of A P))) (P X) . Theorem Set_Of_th4 : (A : Ens) (P : Ens -> Prop) (SUB (Set_Of A P) A) . Definition intersection := [A, B : Ens] (Set_Of A ([X : Ens] (IN X B))). Theorem intersection_th1 : (A, B : Ens) (SUB (intersection A B) A) . Theorem intersection_th2 : (A, B : Ens) (SUB (intersection A B) B) . Theorem intersection_th3 : (A, B, X : Ens) (i : (IN X A)) (j : (IN X B)) (IN X (intersection A B)) . Theorem intersection_th4 : (A, B, C : Ens) (s : (SUB C A)) (t : (SUB C B)) (SUB C (intersection A B)) . Theorem Singleton_th2 : (X : Ens) (Its_nonempty (Singleton X)) . Theorem union_th1 : (A, B : Ens) (X : Ens) (h : (IN X A)) (IN X (union A B)) . Theorem union_th2 : (A, B : Ens) (X : Ens) (h : (IN X B)) (IN X (union A B)) . Theorem union_th3 : (A, B : Ens) (X : Ens) (h : (not (IN X A))) (k : (not (IN X B))) (not (IN X (union A B))) . Theorem union_th4 : (P : Prop) (A, B, X : Ens) (i : (IN X (union A B))) (a : ((IN X A) -> P)) (b : ((IN X B) -> P)) P . Theorem union_refl : (A : Ens) (EQ A (union A A)) . Theorem union_symm : (A, B : Ens) (EQ (union A B) (union B A)) . Definition has_leq_0_elements := Its_empty. Theorem zero_has_leq_0_elements : (has_leq_0_elements Zero) . Definition has_geq_1_elements := [A : Ens] (not (has_leq_0_elements A)). Theorem has_geq_1_elements_th1 : (A : Ens) (X : Ens) (k : (IN X A)) (has_geq_1_elements A) . Theorem Singletons_have_geq_1_elements : (X : Ens) (has_geq_1_elements (Singleton X)) . Definition has_leq_1_elements := [A : Ens] (X, Y : Ens) (k : (IN X A)) (l : (IN Y A)) (EQ X Y). Theorem has_leq_0_elements_implies_leq_1 : (A : Ens) (q : (has_leq_0_elements A)) (has_leq_1_elements A) . Theorem Singletons_have_leq_1_elements : (A : Ens) (has_leq_1_elements (Singleton A)) . Definition has_geq_2_elements := [A : Ens] (not (has_leq_1_elements A)). Theorem has_geq_2_elements_th1 : (A : Ens) (X, Y : Ens) (k : (IN X A)) (l : (IN Y A)) (m : (not (EQ X Y))) (has_geq_2_elements A) . Definition Doubleton := [X : Ens] [Y : Ens] (union (Singleton X) (Singleton Y)). Theorem Doubleton_th1 : (X, Y : Ens) (IN X (Doubleton X Y)) . Theorem Doubleton_th2 : (X, Y : Ens) (IN Y (Doubleton X Y)) . Theorem Doubleton_th3 : (X, Y : Ens) (A : Ens) (iXA : (IN X A)) (iYA : (IN Y A)) (SUB (Doubleton X Y) A) . Theorem Doubleton_th4 : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (m : (not (EQ Z X))) (n : (not (EQ Z Y))) False . Theorem Doubleton_th4_a : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (m : (not (EQ Z X))) (EQ Z Y) . Theorem Doubleton_th4_b : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (n : (not (EQ Z Y))) (EQ Z X) . Theorem distinct_Doubletons_have_geq_2_elements : (X, Y : Ens) (n : (not (EQ X Y))) (has_geq_2_elements (Doubleton X Y)) . Theorem Big_Extensionality : (P : Ens -> Prop) (X, Y : Ens) (p : (P X)) (e : (EQ X Y)) (P Y) . Theorem Substitute : (X, Y : Ens) (P : Ens -> Prop) (e : (EQ X Y)) (p : (P Y)) (P X) . Theorem counting_lem1 : (X, Y : Ens) (m : (has_leq_0_elements X)) (n : (has_geq_1_elements Y)) (not (EQ X Y)) . Theorem counting_lem2 : (X, Y : Ens) (m : (has_leq_1_elements X)) (n : (has_geq_2_elements Y)) (not (EQ X Y)) . Definition First : Ens -> Ens := [X : Ens] (Singleton X). Definition Second : Ens -> Ens := [X : Ens] (Doubleton Zero (Singleton X)). Definition PAIR : Ens -> Ens -> Ens := [X, Y : Ens] (Doubleton (First X) (Second Y)). Theorem First_uniqueness : (A, B : Ens) (m : (EQ (First A) (First B))) (EQ A B) . Theorem Singleton_uniqueness : (A, B : Ens) (m : (EQ (Singleton A) (Singleton B))) (EQ A B) . Record pairwise_EQ [A, B, C, D : Ens] : Prop := { pairwise_EQ_ac : (EQ A C); pairwise_EQ_bd : (EQ B D) }. Theorem Doubleton_uniqueness : (P : Ens -> Prop) (A, B, C, D : Ens) (pA : (P A)) (nB : (not (P B))) (pC : (P C)) (nD : (not (P D))) (e : (EQ (Doubleton A B) (Doubleton C D))) (pairwise_EQ A B C D) . Theorem Second_has_geq_2_elements : (A : Ens) (has_geq_2_elements (Second A)) . Theorem Second_uniqueness : (A, B : Ens) (k : (EQ (Second A) (Second B))) (EQ A B) . Theorem PAIR_uniqueness : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (pairwise_EQ A B C D) . Theorem PAIR_uni_ac : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ A C) . Theorem PAIR_uni_bd : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ B D) . Definition is_a_pair := [M : Ens] (EXISTS ([A : Ens] (EXISTS ([B : Ens] (EQ M (PAIR A B)))))). Theorem a_pair_is_a_pair : (A, B : Ens) (is_a_pair (PAIR A B)) . Theorem a_pair_is_a_pair_th2 : (A, B, U : Ens) (i : (EQ (PAIR A B) U)) (is_a_pair U) . Definition PR1 := [M : Ens] (CHOICE ([A : Ens] (EXISTS ([B : Ens] (EQ M (PAIR A B)))))). Theorem PAIR_proj1_pr1 : (M : Ens) (p : (is_a_pair M)) (EXISTS ([B : Ens] (EQ M (PAIR (PR1 M) B)))) . Definition PR2 := [M : Ens] (CHOICE ([B : Ens] (EQ M (PAIR (PR1 M) B)))). Theorem PAIR_proj_th1 : (M : Ens) (p : (is_a_pair M)) (EQ M (PAIR (PR1 M) (PR2 M))) . Theorem PAIR_proj_th2 : (X, Y : Ens) (pairwise_EQ X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y))) . Theorem PAIR_proj_th3 : (X, Y : Ens) (EQ X (PR1 (PAIR X Y))) . Theorem PAIR_proj_th4 : (X, Y : Ens) (EQ Y (PR2 (PAIR X Y))) . Theorem PAIR_proj_uni : (M : Ens) (m : (is_a_pair M)) (N : Ens) (n : (is_a_pair N)) (e : (EQ (PR1 M) (PR1 N))) (f : (EQ (PR2 M) (PR2 N))) (EQ M N) . Definition Powerset := [X : Ens] (REPLACEMENT ([Y : Ens] (SUB Y X))). Theorem Powerset_pr1 : (X, Y : Ens) (h : (SUB Y X)) (IN Y (Powerset X)) . Theorem Powerset_pr2 : (X, Y : Ens) (i : (IN Y (Powerset X))) (SUB Y X) . Theorem Powerset_th1 : (A : Ens) (IN Zero (Powerset A)) . Theorem Powerset_th2 : (A, X, Y : Ens) (x : (IN X (Powerset A))) (y : (IN Y (Powerset A))) (IN (union X Y) (Powerset A)) . Theorem Powerset_th3 : (A, X, Y : Ens) (x : (IN X (Powerset A))) ((y : (IN Y (Powerset A)))) (IN (intersection X Y) (Powerset A)) . Theorem Powerset_th4 : (A, X : Ens) (x : (IN X A)) (IN (Singleton X) (Powerset A)) . Theorem Powerset_th5 : (A, X, Y : Ens) (x : (IN X A)) (y : (IN Y A)) (IN (Doubleton X Y) (Powerset A)) . Theorem Powerset_th6 : (A, X : Ens) (x : (IN X A)) (IN (Second X) (Powerset (Powerset A))) . Theorem Powerset_th7 : (A, B : Ens) (a : (SUB A B)) (SUB (Powerset A) (Powerset B)) . Definition Element_of_NN := [Y : Ens] (X : Ens) (k : (Contains_NN X)) (IN Y X). Theorem Zero_element_of_NN : (Element_of_NN Zero) . Theorem Nexts_element_of_NN : (A : Ens) (h : (Element_of_NN A)) (Element_of_NN (Next A)) . Definition Set_containing_NN := (CHOICE Contains_NN). Theorem Set_containing_NN_pr : (Contains_NN Set_containing_NN) . Theorem Bounded_NN_pre : (EXISTS ([A : Ens] (Bounded_By A Element_of_NN))) . Theorem Bounded_NN : (Bounded Element_of_NN) . Definition Naturals := (REPLACEMENT Element_of_NN). Theorem Naturals_pr1 : (X : Ens) (Element_of_NN X) -> (IN X Naturals) . Theorem Naturals_pr2 : (X : Ens) (IN X Naturals) -> (Element_of_NN X) . Theorem Zero_in_Naturals : (IN Zero Naturals) . Theorem Nexts_in_Naturals : (A : Ens) (h : (IN A Naturals)) (IN (Next A) Naturals) . Theorem Contains_NN_Naturals : (Contains_NN Naturals) . Theorem Naturals_th1 : (X : Ens) (h : (Contains_NN X)) (SUB Naturals X) . Theorem anything_sub_next_of_itself : (A : Ens) (SUB A (Next A)) . Theorem anything_in_next_of_itself : (A : Ens) (IN A (Next A)) . Definition naturals_induction_nexts := [P : Ens -> Prop] (A : Ens) (h : (IN A Naturals)) (k : (P A)) (P (Next A)). Theorem naturals_inductionA : (P : Ens -> Prop) (IH_zero : (P Zero)) (IH_nexts : (naturals_induction_nexts P)) (B : Ens) (p : (IN B Naturals)) (P B) . Definition in_then_strictsub := [N : Ens] (X : Ens) (IN X N) -> (StrictSUB X N). Definition not_in_itself := [X : Ens] (not (IN X X)). Record naturals_main_ind_hyp [N : Ens] : Prop := { naturals_main_ind1 : (in_then_strictsub N); naturals_main_ind2 : (not_in_itself N) }. Theorem some_things_strictsub_their_nexts : (A : Ens) (h : (not_in_itself A)) (StrictSUB A (Next A)) . Theorem in_then_strictsub_Zero : (X : Ens) (IN X Zero) -> (StrictSUB X Zero) . Theorem zero_not_in_itself : (not_in_itself Zero) . Theorem naturals_main_ind_for_Zero : (naturals_main_ind_hyp Zero) . Theorem naturals_main_induction_next : (A : Ens) (h : (naturals_main_ind_hyp A)) (naturals_main_ind_hyp (Next A)) . Theorem naturals_main_induction_next_1 : (naturals_induction_nexts naturals_main_ind_hyp) . Theorem naturals_main_th1 : (B : Ens) (i : (IN B Naturals)) (naturals_main_ind_hyp B) . Theorem naturals_main_th2_rewrite : (B : Ens) (i : (IN B Naturals)) (A : Ens) (j : (IN A B)) (StrictSUB A B) . Theorem naturals_main_th3_rewrite : (B : Ens) (i : (IN B Naturals)) (not (IN B B)) . Definition Domain_prop := [R : Ens] [X : Ens] (EXISTS ([Y : Ens] (IN (PAIR X Y) R))). Definition Range_prop := [R : Ens] [Y : Ens] (EXISTS ([X : Ens] (IN (PAIR X Y) R))). Definition EV := [R : Ens] [X : Ens] (CHOICE ([Y : Ens] (IN (PAIR X Y) R))). Theorem EV_pr : (R : Ens) (X : Ens) (p : (Domain_prop R X)) (IN (PAIR X (EV R X)) R) . Theorem Domain_prop_bounded : (R : Ens) (Bounded (Domain_prop R)) . Theorem Range_prop_bounded : (R : Ens) (Bounded (Range_prop R)) . Definition Domain := [R : Ens] (REPLACEMENT (Domain_prop R)). Theorem Domain_pr1 : (R : Ens) (X : Ens) (p : (Domain_prop R X)) (IN X (Domain R)) . Theorem Domain_pr2 : (R : Ens) (X : Ens) (i : (IN X (Domain R))) (Domain_prop R X) . Theorem EV_th1 : (R : Ens) (X : Ens) (i : (IN X (Domain R))) (IN (PAIR X (EV R X)) R) . Theorem Domain_th1 : (R : Ens) (X, Y : Ens) (i : (IN (PAIR X Y) R)) (IN X (Domain R)) . Definition Range := [R : Ens] (REPLACEMENT (Range_prop R)). Theorem inverse_EV_th1 : (R : Ens) (Y : Ens) (i : (IN Y (Range R))) (IN (PAIR (inverse_EV R Y) Y) R) . Theorem Range_th1 : (R : Ens) (X, Y : Ens) (i : (IN (PAIR X Y) R)) (IN Y (Range R)) . Theorem EV_in_range : (R, X : Ens) (i : (IN X (Domain R))) (IN (EV R X) (Range R)) . Definition is_a_relation := [R : Ens] (X : Ens) (i : (IN X R)) (is_a_pair X). Definition well_definedness := [F : Ens] (X, Y, Z : Ens) (i : (IN (PAIR X Y) F)) (j : (IN (PAIR X Z) F)) (EQ Y Z). Record is_a_function [F : Ens] : Prop := { function_is_a_relation : (is_a_relation F); function_well_definedness : (well_definedness F) }. Theorem function_sub : (F : Ens) (f : (is_a_function F)) (G : Ens) (s : (SUB G F)) (is_a_function G) . Theorem function_th1 : (F : Ens) (f : (is_a_function F)) (X, Y : Ens) (i : (IN (PAIR X Y) F)) (EQ Y (EV F X)) . Definition Extensionally_equivalent := [F, G : Ens] (X : Ens) (i : (IN X (Domain F))) (j : (IN X (Domain G))) (EQ (EV F X) (EV G X)). Theorem Extensionality_for_functions : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (d : (EQ (Domain F) (Domain G))) (e : (Extensionally_equivalent F G)) (EQ F G) . Theorem function_evaluation : (F, X, Y : Ens) (f : (is_a_function F)) (i : (IN (PAIR X Y) F)) (EQ Y (EV F X)) . Definition restricted_to := [A, F : Ens] (Set_Of F ([M : Ens] (IN (PR1 M) A))). Theorem restricted_to_th5 : (A, F : Ens) (EQ (intersection A (Domain F)) (Domain (restricted_to A F))) . Theorem restricted_to_th9 : (A, F : Ens) (f : (is_a_function F)) (X : Ens) (i : (IN X A)) (j : (IN X (Domain F))) (EQ (EV F X) (EV (restricted_to A F) X)) . Theorem empty_function_function : (is_a_function Zero) . Theorem empty_function_domain : (EQ Zero (Domain Zero)) . Record in_cartesian [A, B, P : Ens] : Prop := { in_cartesian_pair : (is_a_pair P); in_cartesian_pr1 : (IN (PR1 P) A); in_cartesian_pr2 : (IN (PR2 P) B) }. Theorem in_cartesian_bounded : (A, B : Ens) (Bounded (in_cartesian A B)) . Definition Cartesian := [A, B : Ens] (REPLACEMENT (in_cartesian A B)). Theorem Cartesian_construction : (A, B : Ens) (X, Y : Ens) (i : (IN X A)) (j : (IN Y B)) (IN (PAIR X Y) (Cartesian A B)) . Theorem Cartesian_pair_th1 : (A, B, X, Y : Ens) (i : (IN (PAIR X Y) (Cartesian A B))) (IN X A) . Theorem Cartesian_pair_th2 : (A, B, X, Y : Ens) (i : (IN (PAIR X Y) (Cartesian A B))) (IN Y B) . Theorem relations_in_cartesian : (R : Ens) (r : (is_a_relation R)) (SUB R (Cartesian (Domain R) (Range R))) . Theorem cartesian_is_relation : (A, B : Ens) (is_a_relation (Cartesian A B)) . Theorem covering_th1 : (A, B, F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (u : (EQ (Domain F) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (Extensionally_equivalent F G) . Theorem covering_th2 : (A, B, F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (u : (EQ (Domain F) (union A B))) (v : (EQ (Domain G) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (EQ F G) . Theorem glueing_th4 : (F, G : Ens) (EQ (Domain (union F G)) (union (Domain F) (Domain G))) . Theorem glueing_th5 : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (e : (Extensionally_equivalent F G)) (is_a_function (union F G)) . (****** the following are for composition of functions or more generally relations *************************) Record Comp_inter [F, G, X, Y, Z : Ens] : Prop := { Comp_inter_xy : (IN (PAIR X Y) F); Comp_inter_yz : (IN (PAIR Y Z) G) }. Record Comp_prop [F, G, X : Ens] : Prop := { Comp_pair : (is_a_pair X); Comp_intern : (EXISTS ([Y : Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))) }. Definition Comp_INTER := [F, G, X : Ens] (CHOICE ([Y : Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))). Theorem Comp_INTER_th1 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PAIR (PR1 X) (Comp_INTER F G X)) F) . Theorem Comp_INTER_th2 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PAIR (Comp_INTER F G X) (PR2 X)) G) . Theorem composition_bounded_by : (F, G : Ens) (Bounded_By (Cartesian (Domain F) (Range G)) (Comp_prop F G)) . Definition COMP := [F, G : Ens] (REPLACEMENT (Comp_prop F G)). Theorem COMP_th2 : (F, G : Ens) (SUB (COMP F G) (Cartesian (Domain F) (Range G))) . Definition Comp_INTERp := [F, G, X, Y : Ens] (Comp_INTER F G (PAIR X Y)). Theorem COMP_th3p : (F, G, X, Y : Ens) (i : (IN (PAIR X Y) (COMP F G))) (IN (PAIR X (Comp_INTERp F G X Y)) F) . Theorem COMP_th4p : (F, G, X, Y : Ens) (i : (IN (PAIR X Y) (COMP F G))) (IN (PAIR (Comp_INTERp F G X Y) Y) G) . Theorem composition_th2 : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (is_a_function (COMP F G)) . Theorem COMP_th5 : (F, G, X, Y, Z : Ens) (i : (IN (PAIR X Y) F)) (j : (IN (PAIR Y Z) G)) (IN (PAIR X Z) (COMP F G)) . Theorem composition_th3 : (F, G, X : Ens) (i : (IN X (Domain F))) (j : (IN (EV F X) (Domain G))) (IN (PAIR X (EV G (EV F X))) (COMP F G)) . Theorem composition_th4 : (F, G, X : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (i : (IN X (Domain F))) (j : (IN (EV F X) (Domain G))) (EQ (EV (COMP F G) X) (EV G (EV F X))) . Theorem COMP_assoc : (F, G, H : Ens) (EQ (COMP F (COMP G H)) (COMP (COMP F G) H)) . \end{verbatim} \begin{thebibliography}{MM} \bibitem{Alexandre} G. Alexandre. An axiomatisation of intuitionistic Zermelo-Fraenkel set theory: see \newline {\tt http://coq.inria.fr/contribs-eng.html}. \bibitem{Wenzel} M. Wenzel. Article in {\em TPHOLs '99, Nice}, Springer {\sc Lecture Notes in Computer Science}. \bibitem{Werner} B. Werner. Sets in Types, Types in Sets: \newline {\tt http://pauillac.inria.fr/~werner/publis/zfc.ps.gz} \bibitem{Werner2} B. Werner. An encoding of Zermolo-Fraenkel Set Theory in Coq: see \newline {\tt http://coq.inria.fr/contribs-eng.html}. {\sc Some of the main theorem proving systems that I have heard about are listed below.} \bibitem{Coq-ref} Coq system reference manual: \newline {\tt http://coq.inria.fr/doc/main.html}. \bibitem{Coq} Coq system: \newline {\tt http://coq.inria.fr/}. \bibitem{OxfordPage} Formal Methods web page at Oxford (this has a very complete listing of items on the web concerning formal methods): \newline {\tt http://www.afm.sbu.ac.uk/}. \bibitem{ACL2} ACL2 system: \newline {\tt http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html}. \bibitem{HOL} HOL system: \newline {\tt http://www.afm.sbu.ac.uk/archive/formal-methods/hol.html}. \bibitem{IMPS} IMPS system (this seems to be out of commission now)---old address : \newline \verb+ftp://math.harvard.edu/imps/imps_html/imps.html+. \bibitem{Isabelle} Isabelle system : \newline {\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}. \bibitem{Lego} LEGO system : \newline {\tt http://www.dcs.ed.ac.uk/home/lego/}. \bibitem{Mizar} Mizar system : \newline {\tt http://mizar.uw.bialystok.pl/}. \bibitem{JFM} {\em Journal of Formalized Mathematics} : \newline {\tt http://mizar.uw.bialystok.pl/JFM/}. \bibitem{nuprl} Nuprl system: \newline {\tt http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}. \end{thebibliography} \invisible{ *) (**************** here is the full summary of parameters, axioms, definitions and theorems ***** \begin{verbatim} Parameter Ens : Type . Parameter IN : Ens -> Ens -> Prop . Definition SUB := [A, B : Ens] (C : Ens) ((IN C A) -> (IN C B)). Record EQ [A : Ens ; B : Ens] : Prop := { EQ_forwards : (SUB A B); EQ_backwards : (SUB B A) }. Axiom excluded_middle : (P : Prop) (not (not P)) -> P . Theorem false_implies_everything : (P : Prop) (False -> P) . Definition DOESNT_EXIST := [P : Ens -> Prop] ((A : Ens) (not (P A))). Definition EXISTS := [P : Ens -> Prop] (not (DOESNT_EXIST P)). Parameter CHOICE : (P : Ens -> Prop) Ens . Axiom CHOICE_pr : (P : Ens -> Prop) (h : (EXISTS P)) (P (CHOICE P)) . Parameter EmptySet : Ens . Axiom EmptySet_pr : (DOESNT_EXIST ([X : Ens] (IN X EmptySet))) . Definition Bounded_By := [A : Ens] [P : Ens -> Prop] (X : Ens) ((P X) -> (IN X A)). Definition Bounded := [P : Ens -> Prop] (EXISTS ([A : Ens] (Bounded_By A P))). Parameter union : (A, B : Ens) Ens . Axiom union_pr1 : (A, B : Ens) (SUB A (union A B)) . Axiom union_pr2 : (A, B : Ens) (SUB B (union A B)) . Axiom union_pr3 : (A, B, C : Ens) (h : (SUB A C)) (k : (SUB B C)) (SUB (union A B) C) . Record nested_IN [A, B, C : Ens] : Prop := { nested_IN_ab : (IN A B); nested_IN_bc : (IN B C) }. Definition b_in_Union_a := [A, B : Ens] (EXISTS ([C : Ens] (nested_IN B C A))). Axiom Union_bounded : (F : Ens) (Bounded (b_in_Union_a F)) . Parameter Singleton : Ens -> Ens . Axiom Singleton_pr1 : (X : Ens) (IN X (Singleton X)) . Axiom Singleton_pr2 : (X : Ens) (Y : Ens) (h : (IN Y (Singleton X))) (EQ X Y) . Axiom Extensionality : (X, Y, Z : Ens) (h : (EQ X Y)) (k : (IN Y Z)) (IN X Z) . Axiom Powerset_bounded : (X : Ens) (Bounded ([Y : Ens] (SUB Y X))) . Parameter REPLACEMENT : (P : Ens -> Prop) Ens . Axiom REPLACEMENT_pr1 : (P : Ens -> Prop) (b : (Bounded P)) (X : Ens) ((P X) -> (IN X (REPLACEMENT P))) . Axiom REPLACEMENT_pr2 : (P : Ens -> Prop) (b : (Bounded P)) (X : Ens) ((IN X (REPLACEMENT P)) -> (P X)) . Definition Zero := EmptySet. Definition Next : Ens -> Ens := [X : Ens] (union X (Singleton X)). Record Contains_NN [X : Ens] : Prop := { Contains_NN_zero : (IN Zero X); Contains_NN_nexts : (A : Ens)(h : (IN A X))(IN (Next A) X) }. Axiom Infinity_exists : (EXISTS Contains_NN) . Theorem EXISTS_th1 : (P : Ens -> Prop) (X : Ens) (p : (P X)) (EXISTS P) . Theorem SUB_refl : (A : Ens) (SUB A A) . Theorem EQ_refl : (A : Ens) (EQ A A) . Theorem EQ_symm : (A, B : Ens) (EQ A B) -> (EQ B A) . Definition NEQ := [A, B : Ens] (not (EQ A B)). Theorem NEQ_symm : (A, B : Ens) (k : (NEQ A B)) (NEQ B A) . Theorem SUB_trans : (A, B, C : Ens) (h : (SUB A B)) (k : (SUB B C)) (SUB A C) . Theorem EQ_trans : (A, B, C : Ens) (h : (EQ A B)) (k : (EQ B C)) (EQ A C) . Record StrictSUB [A, B : Ens] : Prop := { StrictSUB_sub : (SUB A B); StrictSUB_neq : (not (EQ A B)) }. Theorem StrictSUB_trans1 : (A, B, C : Ens) (h : (StrictSUB A B)) (k : (SUB B C)) (StrictSUB A C) . Theorem EmptySet_th1 : (X : Ens) (h : (IN X EmptySet)) False . Theorem EmptySet_th2 : (A : Ens) (SUB EmptySet A) . Definition Its_empty := [A : Ens] (X : Ens) (not (IN X A)). Theorem its_empty_implies_equals_emptyset : (A : Ens) (k : (Its_empty A)) (EQ A EmptySet) . Theorem Its_empty_emptyset : (Its_empty EmptySet) . Definition Its_nonempty := [A : Ens] (not (Its_empty A)). Theorem Its_nonempty_th1 : (X, A : Ens) (h : (IN X A)) (Its_nonempty A) . Theorem Nothing_strictsub_Zero : (X : Ens) (not (StrictSUB X Zero)) . Theorem Bounded_th1 : (P : Ens -> Prop) (A : Ens) (h : (X : Ens) ((P X) -> (IN X A))) (Bounded P) . Theorem Bounded_th2 : (P : Ens -> Prop) (A : Ens) (h : (Bounded_By A P)) (Bounded P) . Definition Bounded_CHOICE := [P : Ens -> Prop] (REPLACEMENT P). Theorem Bounded_CHOICE_pr : (P : Ens -> Prop) (b : (Bounded P)) (Bounded_By (Bounded_CHOICE P) P) . Definition SUBPROP := [P : Ens -> Prop] [Q : Ens -> Prop] (X : Ens) (P X) -> (Q X). Theorem Bounded_subprops_th1 : (P, Q : Ens -> Prop) (s : (SUBPROP P Q)) (A : Ens) (h : (Bounded_By A Q)) (Bounded_By A P) . Theorem Bounded_subprops_th2 : (P, Q : Ens -> Prop) (s : (SUBPROP P Q)) (b : (Bounded Q)) (Bounded P) . Record Restriction [P : Ens -> Prop ; A : Ens ; X : Ens] : Prop := { remaining_property : (P X); the_restriction : (IN X A) }. Theorem Restriction_bounded : (P : Ens -> Prop) (A : Ens) (Bounded (Restriction P A)) . Definition Set_Of := [A : Ens] [P : Ens -> Prop] (REPLACEMENT (Restriction P A)). Theorem Set_Of_pr1 : (A : Ens) (P : Ens -> Prop) (X : Ens) (Restriction P A X) -> (IN X (Set_Of A P)) . Theorem Set_Of_pr2 : (A : Ens) (P : Ens -> Prop) (X : Ens) (IN X (Set_Of A P)) -> (Restriction P A X) . Theorem Set_Of_th1 : (A : Ens) (P : Ens -> Prop) (X : Ens) (h : (IN X A)) (k : (P X)) (IN X (Set_Of A P)) . Theorem Set_Of_th2 : (A : Ens) (P : Ens -> Prop) (X : Ens) (h : (IN X (Set_Of A P))) (P X) . Theorem Set_Of_th3 : (A : Ens) (P : Ens -> Prop) (X : Ens) (h : (IN X (Set_Of A P))) (IN X A) . Theorem Set_Of_th4 : (A : Ens) (P : Ens -> Prop) (SUB (Set_Of A P) A) . Definition intersection := [A, B : Ens] (Set_Of A ([X : Ens] (IN X B))). Theorem intersection_th1 : (A, B : Ens) (SUB (intersection A B) A) . Theorem intersection_th2 : (A, B : Ens) (SUB (intersection A B) B) . Theorem intersection_th3 : (A, B, X : Ens) (i : (IN X A)) (j : (IN X B)) (IN X (intersection A B)) . Theorem intersection_th4 : (A, B, C : Ens) (s : (SUB C A)) (t : (SUB C B)) (SUB C (intersection A B)) . Definition IntersectionProp := [F : Ens -> Ens] [X : Ens] (Y : Ens) (IN X (F Y)). Definition Intersection_Bounded : (F : Ens -> Ens) (Bounded (IntersectionProp F)) := Intersection_section1_Out. Definition Intersection : (F : Ens -> Ens) Ens := [F : Ens -> Ens] (REPLACEMENT (IntersectionProp F)). Theorem Intersection_pr1 : (F : Ens -> Ens) (X : Ens) (IntersectionProp F X) -> (IN X (Intersection F)) . Theorem Intersection_pr2 : (F : Ens -> Ens) (X : Ens) (IN X (Intersection F)) -> (IntersectionProp F X) . Theorem Intersection_th1 : (F : Ens -> Ens) (X : Ens) (h : ((Y : Ens) (IN X (F Y)))) (IN X (Intersection F)) . Theorem Intersection_th2 : (F : Ens -> Ens) (X : Ens) (Y : Ens) (i : (IN X (Intersection F))) (IN X (F Y)) . Theorem Singleton_th1 : (X, A : Ens) (h : (IN X A)) (SUB (Singleton X) A) . Theorem Singleton_th2 : (X : Ens) (Its_nonempty (Singleton X)) . Theorem union_th1 : (A, B : Ens) (X : Ens) (h : (IN X A)) (IN X (union A B)) . Theorem union_th2 : (A, B : Ens) (X : Ens) (h : (IN X B)) (IN X (union A B)) . Theorem union_th3 : (A, B : Ens) (X : Ens) (h : (not (IN X A))) (k : (not (IN X B))) (not (IN X (union A B))) . Theorem union_th4 : (P : Prop) (A, B, X : Ens) (i : (IN X (union A B))) (a : ((IN X A) -> P)) (b : ((IN X B) -> P)) P . Theorem union_refl : (A : Ens) (EQ A (union A A)) . Theorem union_symm : (A, B : Ens) (EQ (union A B) (union B A)) . Definition Union : (F : Ens) Ens := [F : Ens] (REPLACEMENT (b_in_Union_a F)). Theorem Union_pr1 : (F, X : Ens) (h : (EXISTS ([U : Ens] (nested_IN X U F)))) (IN X (Union F)) . Theorem Union_pr2 : (F, X : Ens) (i : (IN X (Union F))) (EXISTS ([U : Ens] (nested_IN X U F))) . Definition Union_intermediate : (F, X : Ens) (i : (IN X (Union F))) Ens := [F, X : Ens] [i : (IN X (Union F))] (CHOICE ([U : Ens] (nested_IN X U F))). Theorem Union_intermediate_pr : (F, X : Ens) (i : (IN X (Union F))) (nested_IN X (Union_intermediate F X i) F) . Theorem Union_intermediate_th1 : (F, X : Ens) (i : (IN X (Union F))) (IN X (Union_intermediate F X i)) . Theorem Union_intermediate_th2 : (F, X : Ens) (i : (IN X (Union F))) (IN (Union_intermediate F X i) F) . Theorem Union_th1 : (F, X, U : Ens) (h : (IN X U)) (k : (IN U F)) (IN X (Union F)) . Definition has_leq_0_elements := Its_empty. Theorem zero_has_leq_0_elements : (has_leq_0_elements Zero) . Definition has_geq_1_elements := [A : Ens] (not (has_leq_0_elements A)). Definition Choose_an_element : (A : Ens) (k : (has_geq_1_elements A)) Ens := [A : Ens] [k : (has_geq_1_elements A)] (CHOICE ([X : Ens] (IN X A))). Theorem Choose_an_element_pr : (A : Ens) (k : (has_geq_1_elements A)) (IN (Choose_an_element A k) A) . Theorem has_geq_1_elements_th1 : (A : Ens) (X : Ens) (k : (IN X A)) (has_geq_1_elements A) . Theorem Singletons_have_geq_1_elements : (X : Ens) (has_geq_1_elements (Singleton X)) . Definition has_leq_1_elements := [A : Ens] (X, Y : Ens) (k : (IN X A)) (l : (IN Y A)) (EQ X Y). Theorem has_leq_0_elements_implies_leq_1 : (A : Ens) (q : (has_leq_0_elements A)) (has_leq_1_elements A) . Theorem Singletons_have_leq_1_elements : (A : Ens) (has_leq_1_elements (Singleton A)) . Definition has_geq_2_elements := [A : Ens] (not (has_leq_1_elements A)). Theorem has_geq_2_elements_th1 : (A : Ens) (X, Y : Ens) (k : (IN X A)) (l : (IN Y A)) (m : (not (EQ X Y))) (has_geq_2_elements A) . Definition Doubleton := [X : Ens] [Y : Ens] (union (Singleton X) (Singleton Y)). Theorem Doubleton_th1 : (X, Y : Ens) (IN X (Doubleton X Y)) . Theorem Doubleton_th2 : (X, Y : Ens) (IN Y (Doubleton X Y)) . Theorem Doubleton_th3 : (X, Y : Ens) (A : Ens) (iXA : (IN X A)) (iYA : (IN Y A)) (SUB (Doubleton X Y) A) . Theorem Doubleton_th4 : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (m : (not (EQ Z X))) (n : (not (EQ Z Y))) False . Theorem Doubleton_th4_a : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (m : (not (EQ Z X))) (EQ Z Y) . Theorem Doubleton_th4_b : (X, Y : Ens) (Z : Ens) (k : (IN Z (Doubleton X Y))) (n : (not (EQ Z Y))) (EQ Z X) . Theorem distinct_Doubletons_have_geq_2_elements : (X, Y : Ens) (n : (not (EQ X Y))) (has_geq_2_elements (Doubleton X Y)) . Theorem Big_Extensionality : (P : Ens -> Prop) (X, Y : Ens) (p : (P X)) (e : (EQ X Y)) (P Y) . Theorem Substitute : (X, Y : Ens) (P : Ens -> Prop) (e : (EQ X Y)) (p : (P Y)) (P X) . Theorem counting_lem1 : (X, Y : Ens) (m : (has_leq_0_elements X)) (n : (has_geq_1_elements Y)) (not (EQ X Y)) . Theorem counting_lem2 : (X, Y : Ens) (m : (has_leq_1_elements X)) (n : (has_geq_2_elements Y)) (not (EQ X Y)) . Definition First : Ens -> Ens := [X : Ens] (Singleton X). Definition Second : Ens -> Ens := [X : Ens] (Doubleton Zero (Singleton X)). Definition PAIR : Ens -> Ens -> Ens := [X, Y : Ens] (Doubleton (First X) (Second Y)). Theorem First_uniqueness : (A, B : Ens) (m : (EQ (First A) (First B))) (EQ A B) . Theorem Singleton_uniqueness : (A, B : Ens) (m : (EQ (Singleton A) (Singleton B))) (EQ A B) . Record pairwise_EQ [A, B, C, D : Ens] : Prop := { pairwise_EQ_ac : (EQ A C); pairwise_EQ_bd : (EQ B D) }. Theorem Doubleton_uniqueness : (P : Ens -> Prop) (A, B, C, D : Ens) (pA : (P A)) (nB : (not (P B))) (pC : (P C)) (nD : (not (P D))) (e : (EQ (Doubleton A B) (Doubleton C D))) (pairwise_EQ A B C D) . Theorem Second_has_geq_2_elements : (A : Ens) (has_geq_2_elements (Second A)) . Theorem Second_uniqueness : (A, B : Ens) (k : (EQ (Second A) (Second B))) (EQ A B) . Theorem PAIR_uniqueness : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (pairwise_EQ A B C D) . Theorem PAIR_uni_ac : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ A C) . Theorem PAIR_uni_bd : (A, B, C, D : Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ B D) . Definition is_a_pair := [M : Ens] (EXISTS ([A : Ens] (EXISTS ([B : Ens] (EQ M (PAIR A B)))))). Theorem a_pair_is_a_pair : (A, B : Ens) (is_a_pair (PAIR A B)) . Theorem a_pair_is_a_pair_th2 : (A, B, U : Ens) (i : (EQ (PAIR A B) U)) (is_a_pair U) . Definition PR1 := [M : Ens] (CHOICE ([A : Ens] (EXISTS ([B : Ens] (EQ M (PAIR A B)))))). Theorem PAIR_proj1_pr1 : (M : Ens) (p : (is_a_pair M)) (EXISTS ([B : Ens] (EQ M (PAIR (PR1 M) B)))) . Definition PR2 := [M : Ens] (CHOICE ([B : Ens] (EQ M (PAIR (PR1 M) B)))). Theorem PAIR_proj_th1 : (M : Ens) (p : (is_a_pair M)) (EQ M (PAIR (PR1 M) (PR2 M))) . Theorem PAIR_proj_th2 : (X, Y : Ens) (pairwise_EQ X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y))) . Theorem PAIR_proj_th3 : (X, Y : Ens) (EQ X (PR1 (PAIR X Y))) . Theorem PAIR_proj_th4 : (X, Y : Ens) (EQ Y (PR2 (PAIR X Y))) . Theorem PAIR_proj_uni : (M : Ens) (m : (is_a_pair M)) (N : Ens) (n : (is_a_pair N)) (e : (EQ (PR1 M) (PR1 N))) (f : (EQ (PR2 M) (PR2 N))) (EQ M N) . Definition Powerset := [X : Ens] (REPLACEMENT ([Y : Ens] (SUB Y X))). Theorem Powerset_pr1 : (X, Y : Ens) (h : (SUB Y X)) (IN Y (Powerset X)) . Theorem Powerset_pr2 : (X, Y : Ens) (i : (IN Y (Powerset X))) (SUB Y X) . Theorem Powerset_th1 : (A : Ens) (IN Zero (Powerset A)) . Theorem Powerset_th2 : (A, X, Y : Ens) (x : (IN X (Powerset A))) (y : (IN Y (Powerset A))) (IN (union X Y) (Powerset A)) . Theorem Powerset_th3 : (A, X, Y : Ens) (x : (IN X (Powerset A))) ((y : (IN Y (Powerset A)))) (IN (intersection X Y) (Powerset A)) . Theorem Powerset_th4 : (A, X : Ens) (x : (IN X A)) (IN (Singleton X) (Powerset A)) . Theorem Powerset_th5 : (A, X, Y : Ens) (x : (IN X A)) (y : (IN Y A)) (IN (Doubleton X Y) (Powerset A)) . Theorem Powerset_th6 : (A, X : Ens) (x : (IN X A)) (IN (Second X) (Powerset (Powerset A))) . Theorem Powerset_th7 : (A, B : Ens) (a : (SUB A B)) (SUB (Powerset A) (Powerset B)) . Definition Element_of_NN := [Y : Ens] (X : Ens) (k : (Contains_NN X)) (IN Y X). Theorem Zero_element_of_NN : (Element_of_NN Zero) . Theorem Nexts_element_of_NN : (A : Ens) (h : (Element_of_NN A)) (Element_of_NN (Next A)) . Definition Set_containing_NN := (CHOICE Contains_NN). Theorem Set_containing_NN_pr : (Contains_NN Set_containing_NN) . Theorem Bounded_NN_pre : (EXISTS ([A : Ens] (Bounded_By A Element_of_NN))) . Theorem Bounded_NN : (Bounded Element_of_NN) . Definition Naturals := (REPLACEMENT Element_of_NN). Theorem Naturals_pr1 : (X : Ens) (Element_of_NN X) -> (IN X Naturals) . Theorem Naturals_pr2 : (X : Ens) (IN X Naturals) -> (Element_of_NN X) . Theorem Zero_in_Naturals : (IN Zero Naturals) . Theorem Nexts_in_Naturals : (A : Ens) (h : (IN A Naturals)) (IN (Next A) Naturals) . Theorem Contains_NN_Naturals : (Contains_NN Naturals) . Theorem Naturals_th1 : (X : Ens) (h : (Contains_NN X)) (SUB Naturals X) . Theorem anything_sub_next_of_itself : (A : Ens) (SUB A (Next A)) . Theorem anything_in_next_of_itself : (A : Ens) (IN A (Next A)) . Definition naturals_induction_nexts := [P : Ens -> Prop] (A : Ens) (h : (IN A Naturals)) (k : (P A)) (P (Next A)). Theorem naturals_inductionA : (P : Ens -> Prop) (IH_zero : (P Zero)) (IH_nexts : (naturals_induction_nexts P)) (B : Ens) (p : (IN B Naturals)) (P B) . Definition in_then_strictsub := [N : Ens] (X : Ens) (IN X N) -> (StrictSUB X N). Definition not_in_itself := [X : Ens] (not (IN X X)). Record naturals_main_ind_hyp [N : Ens] : Prop := { naturals_main_ind1 : (in_then_strictsub N); naturals_main_ind2 : (not_in_itself N) }. Theorem some_things_strictsub_their_nexts : (A : Ens) (h : (not_in_itself A)) (StrictSUB A (Next A)) . Theorem in_then_strictsub_Zero : (X : Ens) (IN X Zero) -> (StrictSUB X Zero) . Theorem zero_not_in_itself : (not_in_itself Zero) . Theorem naturals_main_ind_for_Zero : (naturals_main_ind_hyp Zero) . Theorem naturals_main_induction_next : (A : Ens) (h : (naturals_main_ind_hyp A)) (naturals_main_ind_hyp (Next A)) . Theorem naturals_main_induction_next_1 : (naturals_induction_nexts naturals_main_ind_hyp) . Theorem naturals_main_th1 : (B : Ens) (i : (IN B Naturals)) (naturals_main_ind_hyp B) . Theorem naturals_main_th2 : (B : Ens) (i : (IN B Naturals)) (in_then_strictsub B) . Theorem naturals_main_th2_rewrite : (B : Ens) (i : (IN B Naturals)) (A : Ens) (j : (IN A B)) (StrictSUB A B) . Theorem naturals_main_th3 : (B : Ens) (i : (IN B Naturals)) (not_in_itself B) . Theorem naturals_main_th3_rewrite : (B : Ens) (i : (IN B Naturals)) (not (IN B B)) . Definition UnionPlus := [F : Ens] (union F (Union F)). Definition Total := [R : Ens] (UnionPlus (UnionPlus (UnionPlus R))). Theorem UnionPlus_th1 : (X, F : Ens) (i : (IN X F)) (IN X (UnionPlus F)) . Theorem UnionPlus_th2 : (X, U, F : Ens) (i : (IN X U)) (j : (IN U F)) (IN X (UnionPlus F)) . Theorem Total_th1 : (X, F : Ens) (i : (IN X F)) (IN X (Total F)) . Theorem Total_th2 : (X, Y, F : Ens) (i : (IN X Y)) (j : (IN Y F)) (IN X (Total F)) . Theorem Total_th3 : (X, Y, Z, F : Ens) (i : (IN X Y)) (j : (IN Y Z)) (k : (IN Z F)) (IN X (Total F)) . Theorem Total_th4 : (X, Y, Z, W, F : Ens) (i : (IN X Y)) (j : (IN Y Z)) (k : (IN Z W)) (l : (IN W F)) (IN X (Total F)) . Theorem Relation_Total_th1 : (R : Ens) (A, B : Ens) (i : (IN (PAIR A B) R)) (IN A (Total R)) . Theorem Relation_Total_th2 : (R : Ens) (A, B : Ens) (i : (IN (PAIR A B) R)) (IN B (Total R)) . Definition Domain_prop := [R : Ens] [X : Ens] (EXISTS ([Y : Ens] (IN (PAIR X Y) R))). Definition Range_prop := [R : Ens] [Y : Ens] (EXISTS ([X : Ens] (IN (PAIR X Y) R))). Definition EV := [R : Ens] [X : Ens] (CHOICE ([Y : Ens] (IN (PAIR X Y) R))). Theorem EV_pr : (R : Ens) (X : Ens) (p : (Domain_prop R X)) (IN (PAIR X (EV R X)) R) . Definition inverse_EV := [R : Ens] [Y : Ens] (CHOICE ([X : Ens] (IN (PAIR X Y) R))). Theorem inverse_EV_pr : (R : Ens) (Y : Ens) (p : (Range_prop R Y)) (IN (PAIR (inverse_EV R Y) Y) R) . Theorem Domain_prop_bounded : (R : Ens) (Bounded (Domain_prop R)) . Theorem Range_prop_bounded : (R : Ens) (Bounded (Range_prop R)) . Definition Domain := [R : Ens] (REPLACEMENT (Domain_prop R)). Theorem Domain_pr1 : (R : Ens) (X : Ens) (p : (Domain_prop R X)) (IN X (Domain R)) . Theorem Domain_pr2 : (R : Ens) (X : Ens) (i : (IN X (Domain R))) (Domain_prop R X) . Theorem EV_th1 : (R : Ens) (X : Ens) (i : (IN X (Domain R))) (IN (PAIR X (EV R X)) R) . Theorem Domain_th1 : (R : Ens) (X, Y : Ens) (i : (IN (PAIR X Y) R)) (IN X (Domain R)) . Definition Range := [R : Ens] (REPLACEMENT (Range_prop R)). Theorem Range_pr1 : (R : Ens) (X : Ens) (p : (Range_prop R X)) (IN X (Range R)) . Theorem Range_pr2 : (R : Ens) (X : Ens) (i : (IN X (Range R))) (Range_prop R X) . Theorem inverse_EV_th1 : (R : Ens) (Y : Ens) (i : (IN Y (Range R))) (IN (PAIR (inverse_EV R Y) Y) R) . Theorem Range_th1 : (R : Ens) (X, Y : Ens) (i : (IN (PAIR X Y) R)) (IN Y (Range R)) . Theorem EV_in_range : (R, X : Ens) (i : (IN X (Domain R))) (IN (EV R X) (Range R)) . Theorem inverse_EV_in_domain : (R, Y : Ens) (i : (IN Y (Range R))) (IN (inverse_EV R Y) (Domain R)) . Definition is_a_relation := [R : Ens] (X : Ens) (i : (IN X R)) (is_a_pair X). Theorem relation_sub : (R : Ens) (r : (is_a_relation R)) (S : Ens) (SUB S R) -> (is_a_relation S) . Definition well_definedness := [F : Ens] (X, Y, Z : Ens) (i : (IN (PAIR X Y) F)) (j : (IN (PAIR X Z) F)) (EQ Y Z). Theorem well_definedness_sub : (F : Ens) (w : (well_definedness F)) (R : Ens) (h : (SUB R F)) (well_definedness R) . Record is_a_function [F : Ens] : Prop := { function_is_a_relation : (is_a_relation F); function_well_definedness : (well_definedness F) }. Theorem function_sub : (F : Ens) (f : (is_a_function F)) (G : Ens) (s : (SUB G F)) (is_a_function G) . Record is_a_function_on [D, F : Ens] : Prop := { function_on_fn : (is_a_function F); function_on_dom : (EQ D (Domain F)) }. Theorem function_is_a_function_on : (F : Ens) (f : (is_a_function F)) (is_a_function_on (Domain F) F) . Theorem function_th1 : (F : Ens) (f : (is_a_function F)) (X, Y : Ens) (i : (IN (PAIR X Y) F)) (EQ Y (EV F X)) . Definition Extensionally_equivalent := [F, G : Ens] (X : Ens) (i : (IN X (Domain F))) (j : (IN X (Domain G))) (EQ (EV F X) (EV G X)). Theorem ex_eq_symm : (F, G : Ens) (Extensionally_equivalent F G) -> (Extensionally_equivalent G F) . Theorem ex_eq_sub : (F, G : Ens) (f : (is_a_function F)) (s : (SUB (Domain F) (Domain G))) (e : (Extensionally_equivalent F G)) (SUB F G) . Theorem Extensionality_for_functions : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (d : (EQ (Domain F) (Domain G))) (e : (Extensionally_equivalent F G)) (EQ F G) . Theorem function_evaluation : (F, X, Y : Ens) (f : (is_a_function F)) (i : (IN (PAIR X Y) F)) (EQ Y (EV F X)) . Definition restricted_to := [A, F : Ens] (Set_Of F ([M : Ens] (IN (PR1 M) A))). Theorem restricted_to_th1 : (A, F : Ens) (U : Ens) (i : (IN U F)) (j : (IN (PR1 U) A)) (IN U (restricted_to A F)) . Theorem restricted_to_th2 : (A, F : Ens) (U : Ens) (i : (IN U (restricted_to A F))) (IN (PR1 U) A) . Theorem restricted_to_th3 : (A, F : Ens) (U : Ens) (i : (IN U (restricted_to A F))) (IN U F) . Theorem restricted_to_th4 : (A, F : Ens) (SUB (restricted_to A F) F) . Theorem restricted_to_th5 : (A, F : Ens) (EQ (intersection A (Domain F)) (Domain (restricted_to A F))) . Theorem restricted_to_th6 : (A, F : Ens) (f : (is_a_function F)) (s : (SUB (Domain F) A)) (SUB F (restricted_to A F)) . Theorem restricted_to_th7 : (A, F : Ens) (f : (is_a_function F)) (s : (SUB (Domain F) A)) (EQ F (restricted_to A F)) . Theorem restricted_to_th8 : (A, F : Ens) (f : (is_a_function F)) (X : Ens) (i : (IN X (intersection A (Domain F)))) (EQ (EV F X) (EV (restricted_to A F) X)) . Theorem restricted_to_th9 : (A, F : Ens) (f : (is_a_function F)) (X : Ens) (i : (IN X A)) (j : (IN X (Domain F))) (EQ (EV F X) (EV (restricted_to A F) X)) . Theorem empty_function_relation : (is_a_relation Zero) . Theorem empty_function_well_definedness : (well_definedness Zero) . Theorem empty_function_function : (is_a_function Zero) . Theorem empty_function_domain_empty : (Its_empty (Domain Zero)) . Theorem empty_function_domain : (EQ Zero (Domain Zero)) . Definition PowerPlus := [A : Ens] (union A (Powerset A)). Theorem PowerPlus_th1 : (A : Ens) (SUB A (PowerPlus A)) . Theorem PowerPlus_th2 : (A : Ens) (SUB (Powerset A) (PowerPlus A)) . Definition PowerTotal := [A : Ens] (Powerset (PowerPlus (PowerPlus A))). Theorem PowerTotal_th1 : (A, X, Y : Ens) (x : (IN X A)) (y : (IN Y A)) (IN (PAIR X Y) (PowerTotal A)) . Theorem PowerTotal_th2 : (A, B, X, Y : Ens) (x : (IN X A)) (y : (IN Y B)) (IN (PAIR X Y) (PowerTotal (union A B))) . Record in_cartesian [A, B, P : Ens] : Prop := { in_cartesian_pair : (is_a_pair P); in_cartesian_pr1 : (IN (PR1 P) A); in_cartesian_pr2 : (IN (PR2 P) B) }. Theorem in_cartesian_bounded : (A, B : Ens) (Bounded (in_cartesian A B)) . Definition Cartesian := [A, B : Ens] (REPLACEMENT (in_cartesian A B)). Theorem Cartesian_pr1 : (A, B : Ens) (M : Ens) (h : (in_cartesian A B M)) (IN M (Cartesian A B)) . Theorem Cartesian_pr2 : (A, B : Ens) (M : Ens) (i : (IN M (Cartesian A B))) (in_cartesian A B M) . Theorem Cartesian_construction : (A, B : Ens) (X, Y : Ens) (i : (IN X A)) (j : (IN Y B)) (IN (PAIR X Y) (Cartesian A B)) . Theorem Cartesian_th1 : (A, B : Ens) (U : Ens) (i : (IN U (Cartesian A B))) (is_a_pair U) . Theorem Cartesian_proj1_th : (A, B, U : Ens) (i : (IN U (Cartesian A B))) (IN (PR1 U) A) . Theorem Cartesian_proj2_th : (A, B, U : Ens) (i : (IN U (Cartesian A B))) (IN (PR2 U) B) . Theorem Cartesian_pair_th1 : (A, B, X, Y : Ens) (i : (IN (PAIR X Y) (Cartesian A B))) (IN X A) . Theorem Cartesian_pair_th2 : (A, B, X, Y : Ens) (i : (IN (PAIR X Y) (Cartesian A B))) (IN Y B) . Theorem relations_in_cartesian : (R : Ens) (r : (is_a_relation R)) (SUB R (Cartesian (Domain R) (Range R))) . Theorem cartesian_is_relation : (A, B : Ens) (is_a_relation (Cartesian A B)) . Theorem cartesian_subs_are_relations : (A, B : Ens) (R : Ens) (s : (SUB R (Cartesian A B))) (is_a_relation R) . Theorem covering_th1 : (A, B, F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (u : (EQ (Domain F) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (Extensionally_equivalent F G) . Theorem covering_th2 : (A, B, F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (u : (EQ (Domain F) (union A B))) (v : (EQ (Domain G) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (EQ F G) . Theorem glueing_th1 : (F, G : Ens) (f : (is_a_relation F)) (g : (is_a_relation G)) (is_a_relation (union F G)) . Theorem glueing_th2 : (F, G : Ens) (SUB (Domain (union F G)) (union (Domain F) (Domain G))) . Theorem glueing_th3 : (F, G : Ens) (SUB (union (Domain F) (Domain G)) (Domain (union F G))) . Theorem glueing_th4 : (F, G : Ens) (EQ (Domain (union F G)) (union (Domain F) (Domain G))) . Theorem glueing_th5 : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (e : (Extensionally_equivalent F G)) (is_a_function (union F G)) . Record Comp_inter [F, G, X, Y, Z : Ens] : Prop := { Comp_inter_xy : (IN (PAIR X Y) F); Comp_inter_yz : (IN (PAIR Y Z) G) }. Record Comp_prop [F, G, X : Ens] : Prop := { Comp_pair : (is_a_pair X); Comp_intern : (EXISTS ([Y : Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))) }. Definition Comp_INTER := [F, G, X : Ens] (CHOICE ([Y : Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))). Theorem Comp_INTER_pr1 : (F, G, X : Ens) (c : (Comp_prop F G X)) (Comp_inter F G (PR1 X) (Comp_INTER F G X) (PR2 X)) . Theorem Comp_INTER_th1 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PAIR (PR1 X) (Comp_INTER F G X)) F) . Theorem Comp_INTER_th2 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PAIR (Comp_INTER F G X) (PR2 X)) G) . Theorem Comp_prop_th1 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PR1 X) (Domain F)) . Theorem Comp_prop_th2 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN (PR2 X) (Range G)) . Theorem Comp_prop_th3 : (F, G, X : Ens) (c : (Comp_prop F G X)) (IN X (Cartesian (Domain F) (Range G))) . Theorem composition_bounded_by : (F, G : Ens) (Bounded_By (Cartesian (Domain F) (Range G)) (Comp_prop F G)) . Theorem composition_bounded : (F, G : Ens) (Bounded (Comp_prop F G)) . Definition COMP := [F, G : Ens] (REPLACEMENT (Comp_prop F G)). Theorem COMP_pr1 : (F, G, X : Ens) (Comp_prop F G X) -> (IN X (COMP F G)) . Theorem COMP_pr2 : (F, G, X : Ens) (IN X (COMP F G)) -> (Comp_prop F G X) . Theorem COMP_th1 : (F, G : Ens) (is_a_relation (COMP F G)) . Theorem COMP_th2 : (F, G : Ens) (SUB (COMP F G) (Cartesian (Domain F) (Range G))) . Theorem COMP_th3 : (F, G, X : Ens) (i : (IN X (COMP F G))) (IN (PAIR (PR1 X) (Comp_INTER F G X)) F) . Theorem COMP_th4 : (F, G, X : Ens) (i : (IN X (COMP F G))) (IN (PAIR (Comp_INTER F G X) (PR2 X)) G) . Definition Comp_INTERp := [F, G, X, Y : Ens] (Comp_INTER F G (PAIR X Y)). Theorem COMP_th3p : (F, G, X, Y : Ens) (i : (IN (PAIR X Y) (COMP F G))) (IN (PAIR X (Comp_INTERp F G X Y)) F) . Theorem COMP_th4p : (F, G, X, Y : Ens) (i : (IN (PAIR X Y) (COMP F G))) (IN (PAIR (Comp_INTERp F G X Y) Y) G) . Theorem composition_well_definedness : (F, G : Ens) (f : (well_definedness F)) (g : (well_definedness G)) (well_definedness (COMP F G)) . Theorem composition_th1 : (F, G : Ens) (f : (well_definedness F)) (g : (well_definedness G)) (is_a_function (COMP F G)) . Theorem composition_th2 : (F, G : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (is_a_function (COMP F G)) . Theorem COMP_th5 : (F, G, X, Y, Z : Ens) (i : (IN (PAIR X Y) F)) (j : (IN (PAIR Y Z) G)) (IN (PAIR X Z) (COMP F G)) . Theorem composition_th3 : (F, G, X : Ens) (i : (IN X (Domain F))) (j : (IN (EV F X) (Domain G))) (IN (PAIR X (EV G (EV F X))) (COMP F G)) . Theorem composition_th4 : (F, G, X : Ens) (f : (is_a_function F)) (g : (is_a_function G)) (i : (IN X (Domain F))) (j : (IN (EV F X) (Domain G))) (EQ (EV (COMP F G) X) (EV G (EV F X))) . Theorem COMP_assoc_th1 : (F, G, H : Ens) (SUB (COMP F (COMP G H)) (COMP (COMP F G) H)) . Theorem COMP_assoc_th2 : (F, G, H : Ens) (SUB (COMP (COMP F G) H) (COMP F (COMP G H))) . Theorem COMP_assoc : (F, G, H : Ens) (EQ (COMP F (COMP G H)) (COMP (COMP F G) H)) . *************************************************) (********* the actual Coq file starts here &&&******) (************************************************) (********** parameters and axioms ***************) (************************************************) Parameter Ens : Type. (*** that was the only time we refer to Type, thus we avoid ``typical ambiguity'' ***) Parameter IN : Ens -> Ens -> Prop. Definition SUB := [A,B: Ens] (C: Ens) ((IN C A) -> (IN C B)). Record EQ [A: Ens; B: Ens] : Prop := { EQ_forwards : (SUB A B); EQ_backwards : (SUB B A) }. Axiom excluded_middle : (P:Prop) (not (not P))-> P. Theorem false_implies_everything : (P : Prop) (False -> P). Proof False_ind. (********* existence definitions **********************) Definition DOESNT_EXIST := [P: Ens -> Prop] ((A : Ens)(not (P A))). Definition EXISTS := [P : Ens -> Prop] (not (DOESNT_EXIST P)). (********* the axiom of choice, applied to the whole Ens *******) Parameter CHOICE : (P: Ens -> Prop) Ens. Axiom CHOICE_pr : (P: Ens -> Prop)(h: (EXISTS P)) (P (CHOICE P)). (**** we need to assume that something exists, for simplicity assume the emptyset *****) Parameter EmptySet : Ens. Axiom EmptySet_pr : (DOESNT_EXIST ([X : Ens] (IN X EmptySet))). (********* we have to define Bounded *********************) Definition Bounded_By := [A : Ens] [P: Ens -> Prop] (X: Ens) ( (P X) -> (IN X A) ). Definition Bounded := [P : Ens -> Prop] (EXISTS ([A: Ens] (Bounded_By A P) ) ). (********** unions of two sets, then big Unions ************) Parameter union : (A,B: Ens) Ens. Axiom union_pr1 : (A, B: Ens) (SUB A (union A B)). Axiom union_pr2 : (A,B : Ens) (SUB B (union A B)). Axiom union_pr3 : (A, B, C: Ens) (h: (SUB A C))(k: (SUB B C)) (SUB (union A B) C). Record nested_IN [A,B,C: Ens] : Prop := { nested_IN_ab : (IN A B); nested_IN_bc : (IN B C) }. Definition b_in_Union_a := [A,B: Ens] (EXISTS ([C: Ens] (nested_IN B C A))). Axiom Union_bounded : (F : Ens) (Bounded (b_in_Union_a F)). (******** singletons ****************) Parameter Singleton : Ens -> Ens. Axiom Singleton_pr1 : (X : Ens) (IN X (Singleton X)). Axiom Singleton_pr2 : (X: Ens)(Y: Ens) (h: (IN Y (Singleton X))) (EQ X Y). (********* extensionality ******************) Axiom Extensionality : (X,Y,Z: Ens)(h: (EQ X Y)) (k: (IN Y Z))(IN X Z). (********* powerset ******************) Axiom Powerset_bounded : (X: Ens) (Bounded ([Y: Ens] (SUB Y X))). (********* replacement axioms *********) Parameter REPLACEMENT : (P: Ens -> Prop) Ens. Axiom REPLACEMENT_pr1 : (P: Ens -> Prop)(b : (Bounded P)) (X : Ens) ( (P X) -> (IN X (REPLACEMENT P)) ). Axiom REPLACEMENT_pr2 : (P: Ens -> Prop)(b : (Bounded P)) (X : Ens) ( (IN X (REPLACEMENT P)) -> (P X) ). (*********** for the natural numbers ***********) Definition Zero := EmptySet. Definition Next : Ens -> Ens := [X : Ens] (union X (Singleton X)). Record Contains_NN [X: Ens] :Prop := { Contains_NN_zero : (IN Zero X); Contains_NN_nexts : (A : Ens) (h: (IN A X))(IN (Next A) X) }. Axiom Infinity_exists: (EXISTS Contains_NN). (****************************************************************) (************** beyond this point the words Axiom, Parameter, ***) (************** Declare don't occur **************************) (****************************************************************) (********************************************) (************* Existence *******************) (********************************************) Section EXISTS_th1_proof. Variable P: Ens -> Prop. Variable X : Ens. Hypothesis p: (P X). Hypothesis h : (DOESNT_EXIST P). Remark step1 : (not (P X)). Proof (h X). Lemma EXISTS_th1_proof_Out : False. Proof (step1 p). End EXISTS_th1_proof. Theorem EXISTS_th1 : (P : Ens -> Prop) (X : Ens ) (p : (P X)) (EXISTS P) . Proof EXISTS_th1_proof_Out. (*****************************************) (********* subset and equality ***********) (*****************************************) Section subset_reflexive. Variable A:Ens. Variable B:Ens. Hypothesis h:(IN B A). Lemma subset_reflexive_Out : (IN B A). Proof h. End subset_reflexive. Theorem SUB_refl : (A:Ens) (SUB A A) . Proof subset_reflexive_Out. Section equality_reflexive. Variable A:Ens. Remark step1 : (SUB A A). Proof (SUB_refl A). Lemma equality_reflexive_Out : (EQ A A). Proof (Build_EQ A A step1 step1). End equality_reflexive. Theorem EQ_refl : (A:Ens) (EQ A A). Proof equality_reflexive_Out. Section equality_symmetric. Variable A:Ens. Variable B:Ens. Hypothesis h: (EQ A B). Remark stepfor : (SUB A B). Proof (EQ_forwards A B h). Remark stepback : (SUB B A). Proof (EQ_backwards A B h). Lemma equality_symmetric_Out : (EQ B A). Proof (Build_EQ B A stepback stepfor). End equality_symmetric. Theorem EQ_symm : (A,B: Ens) (EQ A B) -> (EQ B A). Proof equality_symmetric_Out. (**** NEQ_symm *****) Definition NEQ := [A,B: Ens](not(EQ A B)). Section neq_symm_proof. Variable A: Ens. Variable B: Ens. Hypothesis k : (NEQ A B). Hypothesis m : (EQ B A). Remark step1 : (EQ A B). Proof (EQ_symm B A m). Lemma neq_symm_Out : False. Proof (k step1). End neq_symm_proof. Theorem NEQ_symm : (A,B: Ens) (k: (NEQ A B)) (NEQ B A). Proof neq_symm_Out. (******** transitivity **********) Section SUB_trans_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Hypothesis h: (SUB A B). Hypothesis k : (SUB B C). Variable X : Ens. Hypothesis m: (IN X A). Remark step1 : (IN X B). Proof (h X m). Lemma SUB_trans_proof_Out : (IN X C). Proof (k X step1). End SUB_trans_proof. Theorem SUB_trans : (A,B,C: Ens) (h:(SUB A B)) (k: (SUB B C)) (SUB A C). Proof SUB_trans_proof_Out. Section EQ_trans_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Hypothesis h: (EQ A B). Hypothesis k : (EQ B C). Remark step1 : (SUB A B). Proof (EQ_forwards A B h). Remark step2 : (SUB B A). Proof (EQ_backwards A B h). Remark step3 : (SUB B C). Proof (EQ_forwards B C k). Remark step4 : (SUB C B). Proof (EQ_backwards B C k). Remark step5 : (SUB A C). Proof (SUB_trans A B C step1 step3). Remark step6 : (SUB C A). Proof (SUB_trans C B A step4 step2). Lemma EQ_trans_proof_Out :(EQ A C). Proof (Build_EQ A C step5 step6). End EQ_trans_proof. Theorem EQ_trans: (A,B,C: Ens) (h: (EQ A B)) (k: (EQ B C)) (EQ A C). Proof EQ_trans_proof_Out. (***** StrictSUB *****) Record StrictSUB [A,B: Ens]:Prop := { StrictSUB_sub : (SUB A B); StrictSUB_neq : (not (EQ A B)) }. Section strictsub_trans1_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Hypothesis h: (StrictSUB A B). Hypothesis k: (SUB B C). Remark h1 : (SUB A B). Proof (StrictSUB_sub A B h). Remark h2 : (not (EQ A B)). Proof (StrictSUB_neq A B h). Remark step1 : (SUB A C). Proof (SUB_trans A B C h1 k). Section strictsub_trans1a. Hypothesis m: (EQ A C). Remark step2 : (SUB C A). Proof (EQ_backwards A C m). Remark step3 : (SUB B A). Proof (SUB_trans B C A k step2). Remark step4 : (EQ A B). Proof (Build_EQ A B h1 step3). Lemma strictsub_trans1a_Out : False. Proof (h2 step4). End strictsub_trans1a. Remark step5 : (not (EQ A C)). Proof strictsub_trans1a_Out. Lemma strictsub_trans1_Out : (StrictSUB A C). Proof (Build_StrictSUB A C step1 step5). End strictsub_trans1_proof. Theorem StrictSUB_trans1 : (A,B,C: Ens) (h: (StrictSUB A B)) (k: (SUB B C)) (StrictSUB A C). Proof strictsub_trans1_Out. (***** we should also do StrictSUB_trans2 using assumption StrictSUB B C ***) (*** ??? ***) (***********************************) (********* the empty set ***********) (***********************************) Section emptyset_empty. Variable X: Ens. Hypothesis h : (IN X EmptySet). Lemma emptyset_empty_Out : False. Proof (EmptySet_pr X h). End emptyset_empty. Theorem EmptySet_th1 : (X: Ens) (h: (IN X EmptySet)) False . Proof emptyset_empty_Out. Section emptyset_subset_everything. Variable A: Ens. Section emptyset_subset_everything_2. Variable B: Ens. Hypothesis h: (IN B EmptySet). Remark step1 : False . Proof (EmptySet_th1 B h). Lemma emptyset_subset_everything_2_Out : (IN B A) . Proof (false_implies_everything (IN B A) step1). End emptyset_subset_everything_2. Remark step2 : (B: Ens) (h: (IN B EmptySet)) (IN B A) . Proof emptyset_subset_everything_2_Out. Lemma emptyset_subset_everything_Out : (SUB EmptySet A). Proof step2. End emptyset_subset_everything. Theorem EmptySet_th2 : (A : Ens) (SUB EmptySet A) . Proof emptyset_subset_everything_Out. Definition Its_empty := [A : Ens] (X : Ens) (not (IN X A) ). Section its_empty_implies_equals_emptyset_proof. Variable A: Ens. Hypothesis k: (Its_empty A). Section ieieep1. Variable X: Ens. Hypothesis i: (IN X A). Remark step1_1 : False . Proof (k X i). Lemma ieieep1_Out : (IN X EmptySet). Proof (false_implies_everything (IN X EmptySet) step1_1). End ieieep1. Remark step1 : (SUB A EmptySet). Proof ieieep1_Out. Section ieieep2. Variable X: Ens. Hypothesis i: (IN X EmptySet). Remark step2_1 : False. Proof (EmptySet_th1 X i). Lemma ieieep2_Out : (IN X A). Proof (false_implies_everything (IN X A) step2_1). End ieieep2. Remark step2 : (SUB EmptySet A). Proof ieieep2_Out. Lemma ieieep_Out :(EQ A EmptySet). Proof (Build_EQ A EmptySet step1 step2). End its_empty_implies_equals_emptyset_proof. Theorem its_empty_implies_equals_emptyset : (A: Ens) (k: (Its_empty A)) (EQ A EmptySet). Proof ieieep_Out. Theorem Its_empty_emptyset : (Its_empty EmptySet). Proof EmptySet_th1. Definition Its_nonempty := [A : Ens] (not (Its_empty A)). Section Its_nonempty_proof. Variable X : Ens. Variable A : Ens. Hypothesis h : (IN X A). Hypothesis h2 : (Its_empty A). Definition Its_nonempty_proof_Out : False := (h2 X h). End Its_nonempty_proof. Theorem Its_nonempty_th1 : (X,A: Ens) (h : (IN X A)) (Its_nonempty A). Proof Its_nonempty_proof_Out. (*** nothing StrictSUB Zero ***) Section nothing_strictsub_Zero. Variable X: Ens. Hypothesis h: (StrictSUB X Zero). Remark step1 : (SUB X Zero). Proof (StrictSUB_sub X Zero h). Remark step2 : (Its_empty X). Proof [Y: Ens] [m: (IN Y X)] ( EmptySet_th1 Y (step1 Y m) ). Remark step3 : (EQ X Zero) . Proof (its_empty_implies_equals_emptyset X step2). Definition nothing_strictsub_Zero_Out : False := ((StrictSUB_neq X Zero h) step3 ). End nothing_strictsub_Zero. Theorem Nothing_strictsub_Zero : (X: Ens)(not (StrictSUB X Zero)). Proof nothing_strictsub_Zero_Out. (***********************************) (********* Bounded *****************) (***********************************) Section Bounded_th1_proof. Variable P: Ens -> Prop. Variable A : Ens. Hypothesis h : (X: Ens) ( (P X) -> (IN X A) ). Remark step1 : (Bounded_By A P). Proof h. Definition Bounded_th1_proof_Out : (EXISTS ([A: Ens] (Bounded_By A P) ) ) :=( EXISTS_th1 ([B: Ens] (Bounded_By B P) ) A step1 ). End Bounded_th1_proof. Theorem Bounded_th1 : (P : Ens -> Prop) (A: Ens) (h : (X: Ens) ( (P X) -> (IN X A) )) (Bounded P) . Proof Bounded_th1_proof_Out . Theorem Bounded_th2 : (P : Ens -> Prop) (A: Ens) (h : (Bounded_By A P)) (Bounded P). Proof [P : Ens -> Prop] [A: Ens] [h : (Bounded_By A P)] (Bounded_th1 P A h). Definition Bounded_CHOICE := [P: Ens -> Prop] (REPLACEMENT P). Theorem Bounded_CHOICE_pr : (P: Ens -> Prop) (b : (Bounded P)) (Bounded_By (Bounded_CHOICE P) P). Proof [P: Ens -> Prop][b : (Bounded P)] (REPLACEMENT_pr1 P b). Definition SUBPROP := [P: Ens -> Prop][Q : Ens -> Prop] (X : Ens) (P X) -> (Q X). Section Bounded_subprops1. Variable P: Ens -> Prop. Variable Q : Ens -> Prop. Hypothesis s : (SUBPROP P Q). Variable A : Ens. Hypothesis h : (Bounded_By A Q). Section boundedsubprops1. Variable X : Ens. Hypothesis k : (P X). Remark step1 : (Q X) . Proof (s X k). Definition boundedsubprops1_Out : (IN X A) := (h X step1). End boundedsubprops1. Definition Bounded_subprops1_Out : (Bounded_By A P) := boundedsubprops1_Out. End Bounded_subprops1. Theorem Bounded_subprops_th1 : (P,Q: Ens -> Prop) (s : (SUBPROP P Q)) (A: Ens) (h: (Bounded_By A Q)) (Bounded_By A P). Proof Bounded_subprops1_Out. Section Bounded_subprops2. Variable P: Ens -> Prop. Variable Q : Ens -> Prop. Hypothesis s: (SUBPROP P Q). Hypothesis b: (Bounded Q). Local A : Ens := (Bounded_CHOICE Q). Remark h : (Bounded_By A Q) . Proof (Bounded_CHOICE_pr Q b). Remark step1 : (Bounded_By A P) . Proof (Bounded_subprops_th1 P Q s A h). Lemma Bounded_sub2_Out : (Bounded P). Proof (Bounded_th2 P A step1). End Bounded_subprops2. Theorem Bounded_subprops_th2 : (P,Q : Ens -> Prop) (s : (SUBPROP P Q)) (b: (Bounded Q)) (Bounded P). Proof Bounded_sub2_Out. (************************************************) (************ Restriction ***********************) (***** a more practical form of replacement *****) (************************************************) Record Restriction [P: Ens-> Prop;A: Ens; X : Ens] : Prop := { remaining_property : (P X); the_restriction : (IN X A) }. Section restriction_bounded_proof. Variable P: Ens -> Prop. Variable A : Ens. Local R := (Restriction P A). Remark t : (Bounded_By A R) . Proof [X: Ens] [h: (R X)] (the_restriction P A X h). Definition restriction_bounded_Out : (Bounded R) := (EXISTS_th1 ([Y : Ens] (Bounded_By Y R)) A t). End restriction_bounded_proof. Theorem Restriction_bounded : (P: Ens -> Prop) (A: Ens) (Bounded (Restriction P A)). Proof restriction_bounded_Out. Definition Set_Of := [A: Ens][P: Ens -> Prop] (REPLACEMENT (Restriction P A)). Theorem Set_Of_pr1 : (A: Ens)(P: Ens -> Prop) (X: Ens) (Restriction P A X) -> (IN X (Set_Of A P)). Proof [A: Ens][P: Ens -> Prop] (REPLACEMENT_pr1 (Restriction P A) (Restriction_bounded P A)). Theorem Set_Of_pr2 : (A: Ens)(P: Ens -> Prop) (X: Ens) (IN X (Set_Of A P))-> (Restriction P A X). Proof [A: Ens][P: Ens -> Prop] (REPLACEMENT_pr2 (Restriction P A) (Restriction_bounded P A)). Theorem Set_Of_th1 : (A: Ens)(P: Ens -> Prop) (X: Ens) (h: (IN X A)) (k: (P X)) (IN X (Set_Of A P)). Proof [A: Ens][P: Ens -> Prop] [X: Ens] [h: (IN X A)] [k: (P X)] (Set_Of_pr1 A P X (Build_Restriction P A X k h)). Theorem Set_Of_th2 : (A: Ens)(P: Ens -> Prop) (X: Ens) (h: (IN X (Set_Of A P))) (P X). Proof [A: Ens][P: Ens -> Prop] [X: Ens] [h: (IN X (Set_Of A P))] (remaining_property P A X (Set_Of_pr2 A P X h)). Theorem Set_Of_th3 : (A: Ens)(P: Ens -> Prop) (X: Ens) (h: (IN X (Set_Of A P))) (IN X A). Proof [A: Ens][P: Ens -> Prop] [X: Ens] [h: (IN X (Set_Of A P))] (the_restriction P A X (Set_Of_pr2 A P X h)). Theorem Set_Of_th4 : (A: Ens)(P: Ens -> Prop) (SUB (Set_Of A P) A). Proof Set_Of_th3. (***********************************) (********* Intersection ***********) (***********************************) (******** little intersection *******) Definition intersection := [A,B: Ens] (Set_Of A ([X: Ens] (IN X B))). Theorem intersection_th1 : (A,B: Ens) (SUB (intersection A B) A). Proof [A,B,U: Ens] [i: (IN U (intersection A B))] (Set_Of_th3 A ([X: Ens] (IN X B)) U i). Theorem intersection_th2 : (A,B: Ens) (SUB (intersection A B) B). Proof [A,B,U: Ens] [i: (IN U (intersection A B))] (Set_Of_th2 A ([X: Ens] (IN X B)) U i). Theorem intersection_th3 : (A,B,X: Ens) (i: (IN X A)) (j: (IN X B)) (IN X (intersection A B)). Proof [A,B,X: Ens] [i: (IN X A)] [j: (IN X B)] (Set_Of_th1 A ([U: Ens] (IN U B)) X i j). Section intersection4. Variables A,B,C: Ens. Hypothesis s: (SUB C A). Hypothesis t: (SUB C B). Variable X: Ens. Hypothesis i: (IN X C). Remark step1 : (IN X A). Proof (s X i). Remark step2 : (IN X B). Proof (t X i). Lemma intersection4_Out : (IN X (intersection A B)). Proof (intersection_th3 A B X step1 step2). End intersection4. Theorem intersection_th4: (A,B,C: Ens) (s: (SUB C A)) (t: (SUB C B)) (SUB C (intersection A B)). Proof intersection4_Out. (******** big Intersection *********) Definition IntersectionProp := [F : Ens -> Ens] [X : Ens] (Y : Ens) (IN X (F Y)). Section Intersection_section1. Variable F : Ens -> Ens. Local A := (F EmptySet). Section Intersection_section1_1. Variable Z : Ens. Hypothesis h : (IntersectionProp F Z). Definition Intersection_section1_1_Out : (IN Z A) := (h EmptySet). End Intersection_section1_1. Remark step1 : (Z : Ens) (h : (IntersectionProp F Z)) (IN Z A). Proof Intersection_section1_1_Out. Remark step2 : (Bounded_By A (IntersectionProp F)). Proof step1. Definition Intersection_section1_Out : (Bounded (IntersectionProp F)) := (Bounded_th2 (IntersectionProp F) A step2). End Intersection_section1. Definition Intersection_Bounded : (F : Ens -> Ens) (Bounded (IntersectionProp F)) := Intersection_section1_Out. Definition Intersection : (F: Ens -> Ens) Ens := [F: Ens -> Ens] (REPLACEMENT (IntersectionProp F) ). Theorem Intersection_pr1 : (F: Ens -> Ens) (X : Ens) (IntersectionProp F X) -> (IN X (Intersection F)). Proof [F: Ens -> Ens] (REPLACEMENT_pr1 (IntersectionProp F) (Intersection_Bounded F) ). Theorem Intersection_pr2 : (F: Ens -> Ens) (X : Ens) (IN X (Intersection F)) -> (IntersectionProp F X). Proof [F: Ens -> Ens] (REPLACEMENT_pr2 (IntersectionProp F) (Intersection_Bounded F) ). Theorem Intersection_th1 : (F : Ens -> Ens) (X : Ens) (h: ((Y : Ens) (IN X (F Y))) ) (IN X (Intersection F)). Proof Intersection_pr1. Theorem Intersection_th2 : (F : Ens -> Ens) (X : Ens) (Y: Ens) (i: (IN X (Intersection F))) (IN X (F Y)). Proof [F : Ens -> Ens][X,Y : Ens] [i : (IN X (Intersection F))] (Intersection_pr2 F X i Y). (********************************) (********** Singletons **********) (********************************) Section Singleton_th1_proof. Variable X : Ens. Variable A : Ens. Hypothesis h: (IN X A). Local B := (Singleton X). (* now prove SUB B A *) Section Singleton_th1_sub1. Variable C: Ens. Hypothesis h2 : (IN C B). Remark step1 : (EQ X C) . Proof (Singleton_pr2 X C h2). Remark step2 : (EQ C X) . Proof (EQ_symm X C step1). Definition Singleton_th1_sub1_Out : (IN C A) := (Extensionality C X A step2 h). End Singleton_th1_sub1. Definition Singleton_th1_proof_Out : (SUB B A) := Singleton_th1_sub1_Out. End Singleton_th1_proof. Theorem Singleton_th1 : (X, A : Ens) (h: (IN X A)) (SUB (Singleton X) A). Proof Singleton_th1_sub1_Out. Section Singleton_th2_proof. Variable X : Ens. Local B := (Singleton X). Remark step1 : (IN X B) . Proof (Singleton_pr1 X). Hypothesis h : (Its_empty B). Remark step2 : (IN X B) -> False . Proof (h X). Definition Singleton_th2_proof_Out : False := (step2 step1). End Singleton_th2_proof. Theorem Singleton_th2 : (X : Ens) (Its_nonempty (Singleton X)). Proof Singleton_th2_proof_Out. (***************************************) (********** union and Union ************) (***************************************) (********** union **********) Section union_th1_proof. Variable A: Ens. Variable B: Ens. Local U := (union A B). Variable X : Ens. Hypothesis h : (IN X A). Remark step1 : (SUB A U). Proof (union_pr1 A B). Definition union_th1_Out : (IN X U) := (step1 X h). End union_th1_proof. Theorem union_th1 : (A, B : Ens) (X : Ens ) (h: (IN X A)) (IN X (union A B)). Proof union_th1_Out. Section union_th2_proof. Variable A: Ens. Variable B: Ens. Local U := (union A B). Variable X : Ens. Hypothesis h : (IN X B). Remark step1 : (SUB B U). Proof (union_pr2 A B). Definition union_th2_Out : (IN X U) := (step1 X h). End union_th2_proof. Theorem union_th2 : (A, B : Ens) (X : Ens ) (h: (IN X B)) (IN X (union A B)). Proof union_th2_Out. Section union_th3_proof. Variable A: Ens. Variable B: Ens. Local U := (union A B). Variable X : Ens. Hypothesis h : (not (IN X A)). Hypothesis k : (not (IN X B)). Hypothesis m : (IN X U). Record union_th3_property [Y : Ens] : Prop := { union_th3_property_in_the_union : (IN Y U); union_th3_property_not_equal_X : (not (EQ X Y)) }. Remark step1 : (Bounded_By U union_th3_property). Proof [Y : Ens][h : (union_th3_property Y)] (union_th3_property_in_the_union Y h). Remark b : (Bounded union_th3_property). Proof (Bounded_th2 union_th3_property U step1). Local V := (REPLACEMENT union_th3_property ). Remark V_pr1 : (X : Ens) ((union_th3_property X) -> (IN X V)). Proof (REPLACEMENT_pr1 union_th3_property b). Remark V_pr2 : (X : Ens) ((IN X V) -> (union_th3_property X)). Proof (REPLACEMENT_pr2 union_th3_property b). Section A_sub_V_proof. Variable Z : Ens. Hypothesis h2 : (IN Z A). Section A_sub_V_proof1. Hypothesis h3 : (EQ X Z). Remark step1_1 : (IN X A). Proof (Extensionality X Z A h3 h2). Definition A_sub_V_proof1_Out : False := (h step1_1). End A_sub_V_proof1. Remark step2 : (not (EQ X Z)) . Proof A_sub_V_proof1_Out. Remark step3 : (IN Z U) . Proof (union_th1 A B Z h2). Remark step4 : (union_th3_property Z). Proof (Build_union_th3_property Z step3 step2). Lemma A_sub_V_proof_Out : (IN Z V). Proof (V_pr1 Z step4). End A_sub_V_proof. Remark A_sub_V : (SUB A V). Proof A_sub_V_proof_Out. Section B_sub_V_proof. Variable Z : Ens. Hypothesis h2 : (IN Z B). Section B_sub_V_proof1. Hypothesis h3 : (EQ X Z). Remark step1_1 : (IN X B). Proof (Extensionality X Z B h3 h2). Lemma B_sub_V_proof1_Out : False. Proof (k step1_1). End B_sub_V_proof1. Remark step2 : (not (EQ X Z)). Proof B_sub_V_proof1_Out. Remark step3 : (IN Z U). Proof (union_th2 A B Z h2). Remark step4 : (union_th3_property Z). Proof (Build_union_th3_property Z step3 step2). Definition B_sub_V_proof_Out : (IN Z V) := (V_pr1 Z step4). End B_sub_V_proof. Remark B_sub_V : (SUB B V). Proof B_sub_V_proof_Out. Remark U_sub_V : (SUB U V). Proof (union_pr3 A B V A_sub_V B_sub_V). Remark X_in_V : (IN X V). Proof (U_sub_V X m). Remark step5 : (union_th3_property X). Proof (V_pr2 X X_in_V). Remark step6 : (not (EQ X X)). Proof (union_th3_property_not_equal_X X step5). Remark step7 : (EQ X X). Proof (EQ_refl X). Lemma union_th3_proof_Out : False. Proof (step6 step7). End union_th3_proof. Theorem union_th3 : (A,B: Ens) (X: Ens) (h: (not (IN X A))) (k: (not (IN X B))) (not (IN X (union A B))). Proof union_th3_proof_Out. Section union_th4_proof. Variable P : Prop. Variables A,B,X: Ens. Hypothesis i : (IN X (union A B)). Hypothesis a : ((IN X A) -> P). Hypothesis b : ((IN X B) -> P). Section ut4contra. Hypothesis contra : (not P). Section ut4a. Hypothesis j : (IN X A). Remark step1 : P. Proof (a j). Fact step2 : False. Proof (contra step1). End ut4a. Remark step3 : (not (IN X A)). Proof step2. Section ut4b. Hypothesis k : (IN X B). Remark step4 : P. Proof (b k). Fact step5 : False. Proof (contra step4). End ut4b. Remark step6 : (not (IN X B)). Proof step5. Remark step7 : (not (IN X (union A B))). Proof (union_th3 A B X step3 step6). Fact step8 : False. Proof (step7 i). End ut4contra. Lemma union_th4_Out : P. Proof (excluded_middle P step8). End union_th4_proof. Theorem union_th4 : (P: Prop) (A,B,X: Ens) (i : (IN X (union A B))) (a: ((IN X A)-> P)) (b: ((IN X B) -> P)) P. Proof union_th4_Out. Section union_refl_proof. Variable A: Ens. Local U := (union A A). Remark step1 : (SUB A U). Proof (union_pr1 A A). Remark step2 : (SUB A A). Proof (SUB_refl A). Remark step3 : (SUB U A). Proof (union_pr3 A A A step2 step2). Lemma union_refl_proof_Out : (EQ A U). Proof (Build_EQ A U step1 step3). End union_refl_proof. Theorem union_refl : (A: Ens) (EQ A (union A A)). Proof union_refl_proof_Out. Section union_symm_proof. Variable A : Ens. Variable B : Ens. Local U := (union A B). Local V := (union B A). Remark step1 : (SUB A U). Proof (union_pr1 A B). Remark step2 : (SUB B U). Proof (union_pr2 A B). Remark step3 : (SUB B V). Proof (union_pr1 B A). Remark step4 : (SUB A V). Proof (union_pr2 B A). Remark step5 : (SUB U V). Proof (union_pr3 A B V step4 step3). Remark step6 : (SUB V U). Proof (union_pr3 B A U step2 step1). Lemma union_symm_proof_Out : (EQ U V). Proof (Build_EQ U V step5 step6). End union_symm_proof. Theorem union_symm : (A,B: Ens) (EQ (union A B) (union B A)). Proof union_symm_proof_Out. (********** Union ************) Definition Union : (F: Ens) Ens := [F: Ens] (REPLACEMENT (b_in_Union_a F)). Theorem Union_pr1 : (F,X: Ens) (h: (EXISTS ([U : Ens] (nested_IN X U F)))) (IN X (Union F)). Proof [F,X: Ens] [h: (EXISTS ([U : Ens] (nested_IN X U F)))] (REPLACEMENT_pr1 (b_in_Union_a F) (Union_bounded F) X h). Theorem Union_pr2 : (F,X: Ens) (i: (IN X (Union F))) (EXISTS ([U : Ens] (nested_IN X U F))). Proof [F: Ens] (REPLACEMENT_pr2 (b_in_Union_a F) (Union_bounded F)). Definition Union_intermediate : (F,X: Ens) (i: (IN X (Union F))) Ens := [F,X: Ens] [i: (IN X (Union F))] (CHOICE ([U : Ens] (nested_IN X U F)) ). Theorem Union_intermediate_pr : (F,X: Ens) (i: (IN X (Union F))) (nested_IN X (Union_intermediate F X i) F). Proof [F,X: Ens] [i: (IN X (Union F))] (CHOICE_pr ([U : Ens] (nested_IN X U F)) (Union_pr2 F X i) ). Theorem Union_intermediate_th1: (F,X: Ens) (i: (IN X (Union F))) (IN X (Union_intermediate F X i)). Proof [F,X: Ens] [i: (IN X (Union F))] (nested_IN_ab X (Union_intermediate F X i) F (Union_intermediate_pr F X i)). Theorem Union_intermediate_th2: (F,X: Ens) (i: (IN X (Union F))) (IN (Union_intermediate F X i) F). Proof [F,X: Ens] [i: (IN X (Union F))] (nested_IN_bc X (Union_intermediate F X i) F (Union_intermediate_pr F X i)). Section Union_th1_proof. Variable F : Ens. Variable X: Ens. Variable U : Ens. Hypothesis h: (IN X U). Hypothesis k: (IN U F). Remark step1 : (nested_IN X U F). Proof (Build_nested_IN X U F h k). Remark step2 : (EXISTS ([U1 : Ens] (nested_IN X U1 F))). Proof (EXISTS_th1 ([U1 : Ens] (nested_IN X U1 F)) U step1 ). Lemma union_th1_OutA : (IN X (Union F)). Proof (Union_pr1 F X step2). End Union_th1_proof. Theorem Union_th1 : (F,X,U: Ens) (h: (IN X U)) (k: (IN U F)) (IN X (Union F)). Proof union_th1_OutA. (************************************************) (********** Elementary Counting ************) (************************************************) Definition has_leq_0_elements := Its_empty. (*** recall that this is equal to [A: Ens] (X: Ens) (not (IN X A)) ***) Theorem zero_has_leq_0_elements : (has_leq_0_elements Zero). Proof EmptySet_th1. Definition has_geq_1_elements := [A: Ens] (not (has_leq_0_elements A)). (**** this is equal to EXISTS ([X: Ens] (IN X A)) ****) Definition Choose_an_element : (A:Ens) (k: (has_geq_1_elements A)) Ens := [A:Ens] [k: (has_geq_1_elements A)] (CHOICE ([X: Ens](IN X A)) ). Theorem Choose_an_element_pr : (A: Ens) (k: (has_geq_1_elements A)) (IN (Choose_an_element A k) A). Proof [A:Ens] [k: (has_geq_1_elements A)] (CHOICE_pr ([X: Ens](IN X A)) k). Section given_an_element. Variable A: Ens. Variable X: Ens. Variable k: (IN X A). Hypothesis m : (has_leq_0_elements A). Definition given_an_element_Out : False := (m X k). End given_an_element. Theorem has_geq_1_elements_th1: (A: Ens) (X: Ens) (k: (IN X A)) (has_geq_1_elements A). Proof given_an_element_Out. (**** the next statement was already proved above with different notations but we can just redefine it, coq takes care of the change of notations ! *****) Theorem Singletons_have_geq_1_elements: (X: Ens) (has_geq_1_elements (Singleton X)). Proof Singleton_th2. Definition has_leq_1_elements := [A: Ens] (X, Y : Ens)(k: (IN X A))(l: (IN Y A)) (EQ X Y). Section has_leq_0_implies_leq_1. Variable A: Ens. Hypothesis q: (has_leq_0_elements A). Variable X: Ens. Variable Y: Ens. Hypothesis k: (IN X A). Remark step1 : False. Proof (q X k). Local step2 : (EQ X Y) := (false_implies_everything (EQ X Y) step1). Definition has_leq_0_implies_leq_1_Out : (l: (IN Y A))(EQ X Y) := [l: (IN Y A)] step2. (**** we had to do that above because otherwise the sectioning mechanism would have ignored l which we don't actually use ***) End has_leq_0_implies_leq_1. Theorem has_leq_0_elements_implies_leq_1 : (A: Ens) (q: (has_leq_0_elements A)) (has_leq_1_elements A). Proof has_leq_0_implies_leq_1_Out. Section singletons_have_leq_1_elements_proof. Variable A : Ens. Local S:= (Singleton A). Variable X: Ens. Variable Y: Ens. Hypothesis iXS : (IN X S). Hypothesis iYS : (IN Y S). Local step1 : (EQ A X) := (Singleton_pr2 A X iXS). Local step2: (EQ A Y) := (Singleton_pr2 A Y iYS). Local step3 : (EQ X A):= (EQ_symm A X step1). Definition singletons_have_leq_1_elements_Out : (EQ X Y) := (EQ_trans X A Y step3 step2). End singletons_have_leq_1_elements_proof. Theorem Singletons_have_leq_1_elements : (A: Ens) (has_leq_1_elements (Singleton A)). Proof singletons_have_leq_1_elements_Out. Definition has_geq_2_elements := [A: Ens] (not (has_leq_1_elements A)). Section when_given_two_distinct_elements. Variable A: Ens. Variable X: Ens. Variable Y: Ens. Hypothesis k: (IN X A). Hypothesis l: (IN Y A). Hypothesis m : (not (EQ X Y)). Hypothesis h : (has_leq_1_elements A). Definition when_given_two_distinct_elements_Out: False := (m (h X Y k l)). End when_given_two_distinct_elements. Theorem has_geq_2_elements_th1 : (A: Ens) (X,Y: Ens) (k: (IN X A)) (l: (IN Y A)) (m : (not (EQ X Y))) (has_geq_2_elements A). Proof when_given_two_distinct_elements_Out. (***************************************) (********** Doubletons ************) (***************************************) Definition Doubleton := [X : Ens][Y : Ens] (union (Singleton X) (Singleton Y)). Section doubleton_th1_proof. Variable X: Ens. Variable Y: Ens. Local D := (Doubleton X Y). Local iXsX : (IN X (Singleton X)) := (Singleton_pr1 X). Definition doubleton_th1_Out : (IN X D) := (union_th1 (Singleton X) (Singleton Y) X iXsX). End doubleton_th1_proof. Theorem Doubleton_th1 : (X,Y: Ens) (IN X (Doubleton X Y)). Proof doubleton_th1_Out. Section doubleton_th2_proof. Variable X: Ens. Variable Y: Ens. Local D := (Doubleton X Y). Local iYsY : (IN Y (Singleton Y)) := (Singleton_pr1 Y). Definition doubleton_th2_Out : (IN Y D) := (union_th2 (Singleton X) (Singleton Y) Y iYsY). End doubleton_th2_proof. Theorem Doubleton_th2 : (X,Y: Ens) (IN Y (Doubleton X Y)). Proof doubleton_th2_Out. Section doubleton_th3_proof. Variable X: Ens. Variable Y: Ens. Variable A : Ens. Hypothesis iXA : (IN X A). Hypothesis iYA : (IN Y A). Local D:= (Doubleton X Y). Local sXsubA : (SUB (Singleton X) A) := (Singleton_th1 X A iXA). Local sYsubA : (SUB (Singleton Y) A) := (Singleton_th1 Y A iYA). Definition doubleton_th3_Out : (SUB D A) := (union_pr3 (Singleton X) (Singleton Y) A sXsubA sYsubA). End doubleton_th3_proof. Theorem Doubleton_th3: (X,Y:Ens) (A: Ens) (iXA : (IN X A)) (iYA : (IN Y A)) (SUB (Doubleton X Y) A). Proof doubleton_th3_Out. Section doubleton_th4_proof. Variable X: Ens. Variable Y: Ens. Variable Z: Ens. Hypothesis k: (IN Z (Doubleton X Y)). Hypothesis m : (not (EQ Z X)). Hypothesis n: (not (EQ Z Y)). Local D:= (Doubleton X Y). Local sX := (Singleton X). Local sY := (Singleton Y). Section doubleton_th4_sub1. Hypothesis u: (IN Z sX). Local step1_1 : (EQ X Z) := (Singleton_pr2 X Z u). Local step1_2 : (EQ Z X) := (EQ_symm X Z step1_1). Definition doubleton_th4_sub1_Out : False := (m step1_2). End doubleton_th4_sub1. Local step1 : (not (IN Z sX)) := doubleton_th4_sub1_Out. Section doubleton_th4_sub2. Hypothesis u: (IN Z sY). Local step2_1 : (EQ Y Z) := (Singleton_pr2 Y Z u). Local step2_2 : (EQ Z Y) := (EQ_symm Y Z step2_1). Definition doubleton_th4_sub2_Out : False := (n step2_2). End doubleton_th4_sub2. Local step2 : (not (IN Z sY)) := doubleton_th4_sub2_Out. Local step3 : (not (IN Z D)) := (union_th3 sX sY Z step1 step2). Definition doubleton_th4_Out : False := (step3 k). End doubleton_th4_proof. Theorem Doubleton_th4 : (X,Y: Ens) (Z: Ens) (k: (IN Z (Doubleton X Y))) (m: (not (EQ Z X))) (n: (not (EQ Z Y))) False . Proof doubleton_th4_Out. Section doubleton_th4a_proof. Variable X: Ens. Variable Y: Ens. Variable Z: Ens. Hypothesis k: (IN Z (Doubleton X Y)). Hypothesis m: (not (EQ Z X)). Local step1 : (not (not (EQ Z Y))) := (Doubleton_th4 X Y Z k m). Definition doubleton_th4a_Out: (EQ Z Y) := (excluded_middle (EQ Z Y) step1). End doubleton_th4a_proof. Theorem Doubleton_th4_a : (X,Y: Ens) (Z: Ens) (k: (IN Z (Doubleton X Y))) (m: (not (EQ Z X))) (EQ Z Y). Proof doubleton_th4a_Out. Section doubleton_th4b_proof. Variable X: Ens. Variable Y: Ens. Variable Z: Ens. Hypothesis k: (IN Z (Doubleton X Y)). Hypothesis n: (not (EQ Z Y)). Local step1 : (not (not (EQ Z X))) := [m : (not (EQ Z X))] (Doubleton_th4 X Y Z k m n). Definition doubleton_th4b_Out: (EQ Z X) := (excluded_middle (EQ Z X) step1). End doubleton_th4b_proof. Theorem Doubleton_th4_b : (X,Y: Ens) (Z: Ens) (k: (IN Z (Doubleton X Y))) (n: (not (EQ Z Y))) (EQ Z X). Proof doubleton_th4b_Out. Section distinct_doubletons_have_geq_2_elements_proof. Variable X: Ens. Variable Y : Ens. Hypothesis n : (not (EQ X Y)). Local D := (Doubleton X Y). Hypothesis h : (has_leq_1_elements D). Local iXD : (IN X D) := (Doubleton_th1 X Y). Local iYD : (IN Y D) := (Doubleton_th2 X Y). Local step1 : (EQ X Y):= (h X Y iXD iYD). Definition distinct_doubletons_have_geq_2_elements_Out : False := (n step1). End distinct_doubletons_have_geq_2_elements_proof. Theorem distinct_Doubletons_have_geq_2_elements : (X,Y: Ens) (n : (not (EQ X Y))) (has_geq_2_elements (Doubleton X Y)). Proof distinct_doubletons_have_geq_2_elements_Out. (*******************************************) (************* Big_Extensionality **********) (*******************************************) Section big_extensionality_proof. Variable P : Ens -> Prop. Variable X: Ens. Variable Y : Ens. Hypothesis m: (P X). Hypothesis k: (EQ X Y). Local D := (Doubleton X Y). Local iXD : (IN X D) := (Doubleton_th1 X Y). Local iYD : (IN Y D) := (Doubleton_th2 X Y). Local eYX : (EQ Y X) := (EQ_symm X Y k). Local S := (Set_Of D P). Local iXS : (IN X S) := (Set_Of_th1 D P X iXD m). Local iYS : (IN Y S) := (Extensionality Y X S eYX iXS). Definition big_extensionality_Out : (P Y) := (Set_Of_th2 D P Y iYS). End big_extensionality_proof. Theorem Big_Extensionality: (P: Ens-> Prop) (X,Y: Ens) (p: (P X)) (e : (EQ X Y)) (P Y). Proof big_extensionality_Out. (******* here is perhaps a useful rewrite *****) Theorem Substitute : (X,Y: Ens) (P : Ens -> Prop) (e : (EQ X Y)) (p : (P Y)) (P X). Proof [X,Y: Ens] [P : Ens -> Prop] [e : (EQ X Y)] [p : (P Y)] (Big_Extensionality P Y X p (EQ_symm X Y e)). (*** a few conclusions using Big_Extensionality ***) Section zero_different_from_one. Variable X: Ens. Variable Y: Ens. Hypothesis m: (has_leq_0_elements X). Hypothesis n: (has_geq_1_elements Y). Hypothesis h: (EQ X Y). Local step1 : (has_leq_0_elements Y) := (Big_Extensionality has_leq_0_elements X Y m h). Definition zero_different_from_one_Out : False := (n step1). End zero_different_from_one. Theorem counting_lem1 : (X,Y: Ens) (m : (has_leq_0_elements X)) (n: (has_geq_1_elements Y)) (not (EQ X Y)). Proof zero_different_from_one_Out. Section one_different_from_two. Variable X: Ens. Variable Y: Ens. Hypothesis m: (has_leq_1_elements X). Hypothesis n: (has_geq_2_elements Y). Hypothesis h: (EQ X Y). Local step1 : (has_leq_1_elements Y) := (Big_Extensionality has_leq_1_elements X Y m h). Definition one_different_from_two_Out : False := (n step1). End one_different_from_two. Theorem counting_lem2 : (X,Y: Ens) (m : (has_leq_1_elements X)) (n: (has_geq_2_elements Y)) (not (EQ X Y)). Proof one_different_from_two_Out. (****************************************) (********** PAIR ****************) (****************************************) Definition First : Ens -> Ens := [X: Ens] (Singleton X). Definition Second : Ens -> Ens := [X : Ens] (Doubleton Zero (Singleton X)). Definition PAIR : Ens -> Ens -> Ens := [X,Y:Ens] (Doubleton (First X) (Second Y)). Section first_uniqueness. Variable A: Ens. Variable B: Ens. Hypothesis m: (EQ (First A) (First B)). Local F := (First A). Local G:= (First B). Local FsubG : (SUB F G) := (EQ_forwards F G m). Local iAF : (IN A F) := (Singleton_pr1 A). Local iBF : (IN A G) := (FsubG A iAF). Local step1 : (EQ B A) := (Singleton_pr2 B A iBF). Definition first_uniqueness_Out : (EQ A B) := (EQ_symm B A step1). End first_uniqueness. Theorem First_uniqueness : (A,B: Ens) (m: (EQ (First A) (First B))) (EQ A B). Proof first_uniqueness_Out. Theorem Singleton_uniqueness : (A,B: Ens) (m: (EQ (Singleton A) (Singleton B))) (EQ A B). Proof First_uniqueness. Record pairwise_EQ [A,B,C,D: Ens] : Prop := { pairwise_EQ_ac : (EQ A C); pairwise_EQ_bd : (EQ B D) }. Section doubleton_uniqueness_proof. Variable P : Ens -> Prop. Variable A: Ens. Variable B: Ens. Variable C: Ens. Variable D: Ens. Hypothesis pA : (P A). Hypothesis nB : (not (P B)). Hypothesis pC : (P C). Hypothesis nD : (not (P D)). Hypothesis e: (EQ (Doubleton A B) (Doubleton C D)). Local Doub := (Doubleton C D). Local iA : (IN A (Doubleton A B)) := (Doubleton_th1 A B). Local iB : (IN B (Doubleton A B)) := (Doubleton_th2 A B). Local step1 : (SUB (Doubleton A B) Doub) := (EQ_forwards (Doubleton A B) Doub e). Local iAdoub : (IN A Doub) := (step1 A iA). Local iBdoub : (IN B Doub) := (step1 B iB). Section doubleton_uniqueness_1. Hypothesis k : (EQ A D). (* Definition Big_Extensionality: (P: Ens-> Prop) (X,Y: Ens) (p: (P X)) (e : (EQ X Y)) (P Y) := big_extensionality_Out. *) Local step1_2 : (P D) := (Big_Extensionality P A D pA k). Definition doubleton_uniqueness_1_Out : False := (nD step1_2). End doubleton_uniqueness_1. Local step2 : (NEQ A D) := doubleton_uniqueness_1_Out. Section doubleton_uniqueness_2. Hypothesis k : (EQ B C). Local step1_1 : (EQ C B) := (EQ_symm B C k). (* Definition Big_Extensionality: (P: Ens-> Prop) (X,Y: Ens) (p: (P X)) (e : (EQ X Y)) (P Y) := big_extensionality_Out. *) Local step1_2 : (P B) := (Big_Extensionality P C B pC step1_1). Definition doubleton_uniqueness_2_Out : False := (nB step1_2). End doubleton_uniqueness_2. Local step3 : (NEQ B C) := doubleton_uniqueness_2_Out. (* Definition Doubleton_th4_b : (X,Y: Ens) (Z: Ens) (k: (IN Z (Doubleton X Y))) (n: (not (EQ Z Y))) (EQ Z X) := doubleton_th4b_Out. th4a same but with NEQ Z X and conclusion EQ Z Y *) Local conclusionAC : (EQ A C) := (Doubleton_th4_b C D A iAdoub step2). Local conclusionBD : (EQ B D) := (Doubleton_th4_a C D B iBdoub step3). Definition doubleton_uniqueness_Out : (pairwise_EQ A B C D) := (Build_pairwise_EQ A B C D conclusionAC conclusionBD). End doubleton_uniqueness_proof. Theorem Doubleton_uniqueness : (P : Ens -> Prop) (A,B,C,D: Ens) (pA : (P A)) (nB : (not (P B))) (pC : (P C)) (nD : (not (P D))) (e: (EQ (Doubleton A B) (Doubleton C D))) (pairwise_EQ A B C D). Proof doubleton_uniqueness_Out. Section second_has_geq_2_elements_proof. Variable A: Ens. Hypothesis k: (has_leq_1_elements A). Local sA := (Singleton A). Local E := (Second A). (* recall zero_has_leq_0_elements : (has_leq_0_elements Zero) *) Local step1 : (has_geq_1_elements sA) := (Singletons_have_geq_1_elements A). Section second_geq_2_a. Hypothesis m :(EQ Zero sA). Local stepa_1 : (has_leq_0_elements sA) := (Big_Extensionality has_leq_0_elements Zero sA zero_has_leq_0_elements m). Definition second_geq_2_a_Out : False := (step1 stepa_1). End second_geq_2_a. Local step2 : (NEQ Zero sA) := second_geq_2_a_Out. Definition second_has_geq_2_elements_Out : (has_geq_2_elements E) := (distinct_Doubletons_have_geq_2_elements Zero sA step2). End second_has_geq_2_elements_proof. Theorem Second_has_geq_2_elements : (A: Ens) (has_geq_2_elements (Second A)). Proof second_has_geq_2_elements_Out. Section second_uniqueness_proof. Variable A: Ens. Variable B: Ens. Hypothesis k: (EQ (Second A) (Second B)). (*** recall Second A = Doubleton Zero (Singleton A) ***) Local sA := (Singleton A). Local sB := (Singleton B). Local step1 : (has_geq_1_elements sA) := (Singletons_have_geq_1_elements A). Local step2 : (has_geq_1_elements sB) := (Singletons_have_geq_1_elements B). Local step3 : (pairwise_EQ Zero sA Zero sB) := (Doubleton_uniqueness has_leq_0_elements Zero sA Zero sB zero_has_leq_0_elements step1 zero_has_leq_0_elements step2 k ). Definition second_uniqueness_Out : (EQ A B) := (Singleton_uniqueness A B (pairwise_EQ_bd Zero sA Zero sB step3)). End second_uniqueness_proof. Theorem Second_uniqueness : (A,B: Ens) (k: (EQ (Second A) (Second B))) (EQ A B). Proof second_uniqueness_Out. Section pair_uniqueness_proof. Variable A: Ens. Variable B: Ens. Variable C: Ens. Variable D: Ens. Hypothesis e: (EQ (PAIR A B) (PAIR C D)). Local fA := (First A). Local fC := (First C). Local secB := (Second B). Local secD := (Second D). Local step1 : (has_leq_1_elements fA) := (Singletons_have_leq_1_elements A). Local step2 : (has_leq_1_elements fC) := (Singletons_have_leq_1_elements C). Local step3 : (has_geq_2_elements secB) := (Second_has_geq_2_elements B). Local step4 : (has_geq_2_elements secD) := (Second_has_geq_2_elements D). Local step5 : (pairwise_EQ fA secB fC secD) := (Doubleton_uniqueness has_leq_1_elements fA secB fC secD step1 step3 step2 step4 e ). Local step6 : (EQ fA fC) := (pairwise_EQ_ac fA secB fC secD step5). Local step7 : (EQ secB secD) := (pairwise_EQ_bd fA secB fC secD step5). Local step8 : (EQ A C) := (First_uniqueness A C step6). Local step9 : (EQ B D) := (Second_uniqueness B D step7). Definition pair_uniqueness_Out : (pairwise_EQ A B C D) := (Build_pairwise_EQ A B C D step8 step9). End pair_uniqueness_proof. (* ?PAIR *) Theorem PAIR_uniqueness : (A,B,C,D : Ens) (e: (EQ (PAIR A B) (PAIR C D))) (pairwise_EQ A B C D). Proof pair_uniqueness_Out. Theorem PAIR_uni_ac : (A,B,C,D: Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ A C). Proof [A,B,C,D: Ens] [e : (EQ (PAIR A B) (PAIR C D))] (pairwise_EQ_ac A B C D (PAIR_uniqueness A B C D e)). Theorem PAIR_uni_bd : (A,B,C,D: Ens) (e : (EQ (PAIR A B) (PAIR C D))) (EQ B D). Proof [A,B,C,D: Ens] [e : (EQ (PAIR A B) (PAIR C D))] (pairwise_EQ_bd A B C D (PAIR_uniqueness A B C D e)). Definition is_a_pair := [M : Ens] (EXISTS ([A: Ens] (EXISTS ([B: Ens] (EQ M (PAIR A B) ) ) ) )). Section a_pair_is_a_pair_proof. Variable A: Ens. Variable B: Ens. Local M := (PAIR A B). Local step1 : (EQ M (PAIR A B)) := (EQ_refl M). Local step2 : (EXISTS ([B1: Ens] (EQ M (PAIR A B1) ) ) ) := (EXISTS_th1 ([B1: Ens] (EQ M (PAIR A B1) ) ) B step1). Definition a_pair_is_a_pair_Out : (is_a_pair M) := (EXISTS_th1 ([A1: Ens] (EXISTS ([B1: Ens] (EQ M (PAIR A1 B1) ) ) ) ) A step2 ). End a_pair_is_a_pair_proof. Theorem a_pair_is_a_pair : (A,B: Ens) (is_a_pair (PAIR A B)). Proof a_pair_is_a_pair_Out. Theorem a_pair_is_a_pair_th2 : (A,B,U: Ens) (i : (EQ (PAIR A B) U)) (is_a_pair U). Proof [A,B,U: Ens] [i : (EQ (PAIR A B) U)] (Big_Extensionality ([V: Ens] (is_a_pair V)) (PAIR A B) U (a_pair_is_a_pair A B) i). (******* projections *******) Definition PR1 := [M : Ens] (CHOICE ([A: Ens] (EXISTS ([B: Ens] (EQ M (PAIR A B) ) ) ) ) ). Theorem PAIR_proj1_pr1 : (M : Ens) (p: (is_a_pair M)) (EXISTS ([B: Ens] (EQ M (PAIR (PR1 M) B) ) ) ) . Proof [M : Ens] [p : (is_a_pair M )] (CHOICE_pr ([A: Ens] (EXISTS ([B: Ens] (EQ M (PAIR A B) ) ) ) ) p ). Definition PR2 := [M : Ens] (CHOICE ([B: Ens] (EQ M (PAIR (PR1 M) B) ) ) ). Theorem PAIR_proj_th1 : (M: Ens) (p: (is_a_pair M)) (EQ M (PAIR (PR1 M) (PR2 M) ) ). Proof [M : Ens] [p : (is_a_pair M )] (CHOICE_pr ([B: Ens] (EQ M (PAIR (PR1 M) B) ) ) (PAIR_proj1_pr1 M p)). Section pair_proj2_proof. Variables X,Y: Ens. Local M := (PAIR X Y). Remark step1 : (is_a_pair M). Proof (a_pair_is_a_pair X Y). Remark step2 : (EQ M (PAIR (PR1 M) (PR2 M))). Proof (PAIR_proj_th1 M step1). Lemma pair_proj2_Out : (pairwise_EQ X Y (PR1 M)(PR2 M)). Proof (PAIR_uniqueness X Y (PR1 M)(PR2 M) step2). End pair_proj2_proof. Theorem PAIR_proj_th2 : (X,Y : Ens) (pairwise_EQ X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)) ). Proof pair_proj2_Out. Theorem PAIR_proj_th3 : (X,Y: Ens) (EQ X (PR1 (PAIR X Y))). Proof [X,Y: Ens] (pairwise_EQ_ac X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)) (PAIR_proj_th2 X Y) ). Theorem PAIR_proj_th4 : (X,Y: Ens) (EQ Y (PR2 (PAIR X Y))). Proof [X,Y: Ens] (pairwise_EQ_bd X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)) (PAIR_proj_th2 X Y) ). Section PAIR_proj_uni_proof. Variable M : Ens. Hypothesis m : (is_a_pair M). Variable N : Ens. Hypothesis n : (is_a_pair N). Hypothesis e : (EQ (PR1 M) (PR1 N)). Hypothesis f : (EQ (PR2 M) (PR2 N)). Local M1 := (PR1 M). Local M2 := (PR2 M). Local N1 := (PR1 N). Local N2 := (PR2 N). Local M12 := (PAIR M1 M2). Local N12 := (PAIR N1 N2). Local U := (PAIR M1 N2). Local step1 : (EQ M12 M12) := (EQ_refl M12). Local step2 : (EQ M12 U) := (Big_Extensionality ([X: Ens] (EQ M12 (PAIR M1 X))) M2 N2 step1 f). Local step3 : (EQ U U) := (EQ_refl U). Local step4 : (EQ U N12) := (Big_Extensionality ([X: Ens] (EQ U (PAIR X N2) )) M1 N1 step3 e). Local step5 : (EQ M12 N12) := (EQ_trans M12 U N12 step2 step4). Local step6 : (EQ M M12) := (PAIR_proj_th1 M m). Local step7 : (EQ N N12) := (PAIR_proj_th1 N n). Local step8 : (EQ N12 N) := (EQ_symm N N12 step7). Local step9 : (EQ M N12) := (EQ_trans M M12 N12 step6 step5). Definition PAIR_proj_uni_Out : (EQ M N) :=(EQ_trans M N12 N step9 step8). End PAIR_proj_uni_proof. (***** PAIR_proj_uni says that if two pairs have the same projections then they are equal *******) Theorem PAIR_proj_uni: (M : Ens) (m : (is_a_pair M)) (N : Ens) (n : (is_a_pair N)) (e : (EQ (PR1 M) (PR1 N))) (f : (EQ (PR2 M) (PR2 N))) (EQ M N). Proof PAIR_proj_uni_Out. (*************************************) (************ Powerset **************) (*************************************) Definition Powerset := [X: Ens] (REPLACEMENT ([Y: Ens] (SUB Y X)) ). Theorem Powerset_pr1 : (X,Y:Ens) (h: (SUB Y X)) (IN Y (Powerset X)). Proof [X: Ens] (REPLACEMENT_pr1 ([Y: Ens] (SUB Y X)) (Powerset_bounded X)). Theorem Powerset_pr2 : (X,Y: Ens) (i: (IN Y (Powerset X))) (SUB Y X). Proof [X: Ens] (REPLACEMENT_pr2 ([Y: Ens] (SUB Y X)) (Powerset_bounded X)). Section power0. Variable A: Ens. Remark step1 : (SUB Zero A). Proof (EmptySet_th2 A). Lemma power0_Out : (IN Zero (Powerset A)). Proof (Powerset_pr1 A Zero step1). End power0. Theorem Powerset_th1 : (A: Ens) (IN Zero (Powerset A)). Proof power0_Out. Section power1. Variables A,X,Y: Ens. Hypothesis x: (IN X (Powerset A)). Hypothesis y: (IN Y (Powerset A)). Remark step1 : (SUB X A). Proof (Powerset_pr2 A X x). Remark step2 : (SUB Y A). Proof (Powerset_pr2 A Y y). Remark step3 : (SUB (union X Y) A). Proof (union_pr3 X Y A step1 step2). Lemma power1_Out1 : (IN (union X Y) (Powerset A)). Proof (Powerset_pr1 A (union X Y) step3). Remark step4 : (SUB (intersection X Y) X). Proof (intersection_th1 X Y). Remark step5 : (SUB (intersection X Y) A). Proof (SUB_trans (intersection X Y) X A step4 step1). Lemma power1_Out2 : (IN (intersection X Y) (Powerset A)). Proof (Powerset_pr1 A (intersection X Y) step5). End power1. Theorem Powerset_th2 : (A,X,Y: Ens) (x: (IN X (Powerset A))) (y : (IN Y (Powerset A))) (IN (union X Y) (Powerset A)). Proof power1_Out1. Theorem Powerset_th3 : (A,X,Y: Ens) (x: (IN X (Powerset A))) (* (y : (IN Y (Powerset A))) *) (IN (intersection X Y) (Powerset A)). Proof power1_Out2. Section power2. Variables A,X: Ens. Hypothesis i: (IN X A). Remark step1 : (SUB (Singleton X) A). Proof (Singleton_th1 X A i). Lemma power2_Out : (IN (Singleton X) (Powerset A)). Proof (Powerset_pr1 A (Singleton X) step1). End power2. Theorem Powerset_th4 : (A,X : Ens) (x: (IN X A)) (IN (Singleton X) (Powerset A)). Proof power2_Out. Section power3. Variables A,X,Y: Ens. Hypothesis x: (IN X A). Hypothesis y: (IN Y A). Remark step1 : (IN (Singleton X) (Powerset A)). Proof (Powerset_th4 A X x). Remark step2 : (IN (Singleton Y) (Powerset A)). Proof (Powerset_th4 A Y y). Lemma power3_Out : (IN (Doubleton X Y) (Powerset A)). Proof (Powerset_th2 A (Singleton X) (Singleton Y) step1 step2). End power3. Theorem Powerset_th5: (A,X,Y: Ens) (x: (IN X A)) (y: (IN Y A)) (IN (Doubleton X Y) (Powerset A)). Proof power3_Out. Section power4. Variables A,X : Ens. Hypothesis x : (IN X A). Local sX := (Singleton X). Local P := (Powerset A). Remark step1 : (IN Zero P). Proof (Powerset_th1 A). Remark step2 : (IN sX P). Proof (Powerset_th4 A X x). Lemma power4_Out : (IN (Second X) (Powerset P)). Proof (Powerset_th5 P Zero sX step1 step2). End power4. Theorem Powerset_th6 : (A,X: Ens) (x: (IN X A)) (IN (Second X) (Powerset (Powerset A))). Proof power4_Out. Section power5. Variables A,B: Ens. Hypothesis a: (SUB A B). Variable X : Ens. Hypothesis x: (IN X (Powerset A)). Remark step1 : (SUB X A). Proof (Powerset_pr2 A X x). Remark step2 : (SUB X B). Proof (SUB_trans X A B step1 a). Lemma power5_Out : (IN X (Powerset B)). Proof (Powerset_pr1 B X step2). End power5. Theorem Powerset_th7 : (A,B: Ens) (a: (SUB A B)) (SUB (Powerset A) (Powerset B)). Proof power5_Out. (*********************************************) (********** Naturals part 1 ************) (*********************************************) Definition Element_of_NN := [Y : Ens] (X : Ens) (k : (Contains_NN X)) (IN Y X). Section Zero_element_of_NN_proof. Variable X:Ens. Hypothesis k: (Contains_NN X). Definition Zero_element_of_NN_proof_Out : (IN Zero X) := (Contains_NN_zero X k). End Zero_element_of_NN_proof. Theorem Zero_element_of_NN : (Element_of_NN Zero). Proof Zero_element_of_NN_proof_Out. Section Nexts_element_of_NN_proof. Variable A:Ens. Hypothesis h: (Element_of_NN A). Variable X:Ens. Hypothesis k: (Contains_NN X). Local N := (Next A). Local j : (IN A X) := (h X k). Definition Nexts_element_of_NN_proof_Out : (IN N X) := (Contains_NN_nexts X k A j). End Nexts_element_of_NN_proof. Theorem Nexts_element_of_NN : (A: Ens) (h: (Element_of_NN A)) (Element_of_NN (Next A)). Proof Nexts_element_of_NN_proof_Out. Definition Set_containing_NN := (CHOICE Contains_NN). Theorem Set_containing_NN_pr : (Contains_NN Set_containing_NN). Proof (CHOICE_pr Contains_NN Infinity_exists). Section Bounded_NN_proof. Hypothesis u : (DOESNT_EXIST ([A:Ens] (Bounded_By A Element_of_NN))). Local step1 : (A: Ens) (not (Bounded_By A Element_of_NN)) := u. Local B : Ens := Set_containing_NN. Local v: (Contains_NN B) := Set_containing_NN_pr. Section Bounded_NN_proof2. Variable Z : Ens. Hypothesis w : (Element_of_NN Z). Definition Bounded_NN_proof2_Out : (IN Z B) := (w B v). End Bounded_NN_proof2. Local step2 : (Bounded_By B Element_of_NN) := Bounded_NN_proof2_Out. Definition Bounded_NN_proof_Out : False := (step1 B step2). End Bounded_NN_proof. Theorem Bounded_NN_pre : (EXISTS ([A:Ens] (Bounded_By A Element_of_NN))). Proof Bounded_NN_proof_Out. Theorem Bounded_NN : (Bounded Element_of_NN). Proof Bounded_NN_pre. Definition Naturals := (REPLACEMENT Element_of_NN). Theorem Naturals_pr1 : (X: Ens) (Element_of_NN X) -> (IN X Naturals). Proof (REPLACEMENT_pr1 Element_of_NN Bounded_NN ). Theorem Naturals_pr2 : (X: Ens) (IN X Naturals) -> (Element_of_NN X). Proof (REPLACEMENT_pr2 Element_of_NN Bounded_NN ). (* Now prove Contains_NN Naturals *) (* prove the two inductive properties separately *) Theorem Zero_in_Naturals : (IN Zero Naturals). Proof (Naturals_pr1 Zero Zero_element_of_NN). Theorem Nexts_in_Naturals : (A: Ens) (h: (IN A Naturals)) (IN (Next A) Naturals). Proof [A: Ens][h: (IN A Naturals)] (Naturals_pr1 (Next A) ( Nexts_element_of_NN A (Naturals_pr2 A h) )). Theorem Contains_NN_Naturals : (Contains_NN Naturals). Proof (Build_Contains_NN Naturals Zero_in_Naturals Nexts_in_Naturals). Section Naturals_th1_proof. Variable X : Ens. Hypothesis h: (Contains_NN X). Variable B: Ens. Hypothesis k: (IN B Naturals). Local step1 : (Element_of_NN B) := (Naturals_pr2 B k). Definition Naturals_th1_proof_Out : (IN B X) := (step1 X h). End Naturals_th1_proof. Theorem Naturals_th1 : (X: Ens) (h: (Contains_NN X)) (SUB Naturals X). Proof Naturals_th1_proof_Out. Section A_sub_next_A_proof. Variable A: Ens. Local N := (Next A). (* = (union A (Singleton A)) *) Definition A_sub_next_A_Out : (SUB A N) := (union_pr1 A (Singleton A)). End A_sub_next_A_proof. Theorem anything_sub_next_of_itself : (A: Ens) (SUB A (Next A)). Proof A_sub_next_A_Out. Section A_in_next_A_proof. Variable A :Ens. Local N:= (Next A). Local step1 : (IN A (Singleton A)) := (Singleton_pr1 A). Definition A_in_next_A_Out : (IN A N) := (union_th2 A (Singleton A) A step1). End A_in_next_A_proof. Theorem anything_in_next_of_itself : (A: Ens) (IN A (Next A)). Proof A_in_next_A_Out. (**** now we do some inductions on naturals ****) Section naturals_inductionA_proof. Variable P : Ens->Prop. Hypothesis IH_zero : (P Zero). Hypothesis IH_nexts : (A: Ens) (h: (IN A Naturals)) (k: (P A)) (P (Next A)). Local S := (Set_Of Naturals P). Local step1 : (IN Zero S) := (Set_Of_th1 Naturals P Zero Zero_in_Naturals IH_zero). Local step2 : (SUB S Naturals) := (Set_Of_th4 Naturals P). Local step3 : (A: Ens)(h: (IN A S))(P A) := [A: Ens][h: (IN A S)] (Set_Of_th2 Naturals P A h). Local step4: (A: Ens)(h: (IN A S))(P (Next A)) := [A: Ens][h: (IN A S)] (IH_nexts A (step2 A h) (step3 A h) ). Local step5 : (B: Ens) (h: (IN B Naturals)) (k: (P B)) (IN B S) := [B: Ens][h: (IN B Naturals)][k: (P B)] (Set_Of_th1 Naturals P B h k). Section naturals_inductionA1. Variable A: Ens. Hypothesis h: (IN A S). Local N:= (Next A). Local step1_1 : (P N) := (step4 A h). Local step1_2 : (IN N Naturals) := (Nexts_in_Naturals A (step2 A h)). Definition naturals_inductionA1_Out : (IN N S) := (step5 N step1_2 step1_1). End naturals_inductionA1. Local step6 : (A: Ens) (h:(IN A S))(IN (Next A) S) := naturals_inductionA1_Out. Local step7 : (Contains_NN S) := (Build_Contains_NN S step1 step6). Variable B: Ens. Hypothesis p: (IN B Naturals). Local step8 : (Element_of_NN B):= (Naturals_pr2 B p). Local step9 : (IN B S) := (step8 S step7 ). Definition naturals_inductionA_Out : (P B) := (step3 B step9). End naturals_inductionA_proof. Definition naturals_induction_nexts := [P : Ens -> Prop] (A: Ens) (h: (IN A Naturals))(k: (P A)) (P (Next A)). Theorem naturals_inductionA : (P : Ens->Prop) (IH_zero : (P Zero)) (IH_nexts : (naturals_induction_nexts P)) (B: Ens) (p: (IN B Naturals)) (P B). Proof naturals_inductionA_Out. (* prove some properties of naturals by induction *) Definition in_then_strictsub:= [N: Ens] (X: Ens) (IN X N) -> (StrictSUB X N). Definition not_in_itself := [X: Ens] (not (IN X X)). Record naturals_main_ind_hyp [N: Ens] : Prop := { naturals_main_ind1 : (in_then_strictsub N); naturals_main_ind2 : (not_in_itself N) }. (**** now we prove that if A is not in itself then A strictsub (Next A) *******) Section strictsub_next_proof. Variable A: Ens. Hypothesis h: (not_in_itself A). Local N := (Next A). Local step1 : (SUB A N) := (anything_sub_next_of_itself A). Section strictsub_next1. Hypothesis k: (EQ A N). Local step2 : (SUB N A) := (EQ_backwards A N k). Local step3 : (IN A N) := (anything_in_next_of_itself A). Local step4 : (IN A A) := (step2 A step3). Definition strictsub_next1_Out : False := (h step4). End strictsub_next1. Local step5 : (not (EQ A N)) := strictsub_next1_Out. Definition strictsub_next_Out : (StrictSUB A N) := (Build_StrictSUB A N step1 step5). End strictsub_next_proof. Theorem some_things_strictsub_their_nexts : (A: Ens) (h: (not_in_itself A)) (StrictSUB A (Next A)). Proof strictsub_next_Out. (* now we prove by induction the in_then_strictsub property for Naturals *) Section in_then_strictsub_Zero_proof. Variable X: Ens. Hypothesis h: (IN X Zero). Local step1 : False := (EmptySet_th1 X h). Definition in_iff_strictsub_Zero_Out : (StrictSUB X Zero) := (false_implies_everything (StrictSUB X Zero) step1). End in_then_strictsub_Zero_proof. Theorem in_then_strictsub_Zero : (X: Ens) (IN X Zero) -> (StrictSUB X Zero). Proof in_iff_strictsub_Zero_Out. Section not_in_itself_Zero. Hypothesis h: (IN Zero Zero). Definition not_in_itself_Zero_Out : False := (EmptySet_th1 Zero h). End not_in_itself_Zero. Theorem zero_not_in_itself : (not_in_itself Zero). Proof not_in_itself_Zero_Out. Theorem naturals_main_ind_for_Zero : (naturals_main_ind_hyp Zero) . Proof (Build_naturals_main_ind_hyp Zero in_then_strictsub_Zero zero_not_in_itself ). Section naturals_main_induction_step. Variable A : Ens. Hypothesis h : (naturals_main_ind_hyp A). Local h1 : (in_then_strictsub A) := (naturals_main_ind1 A h). Local h2 : (not_in_itself A) := (naturals_main_ind2 A h). Local N := (Next A). Local in_A_N : (IN A N) := (anything_in_next_of_itself A). Local sub_A_N : (SUB A N) := (anything_sub_next_of_itself A). Section naturals_main_induction2. Hypothesis k: (IN N N). Section naturals_main_induction2a. Hypothesis l: (EQ A N). Local step2a1 : (IN A N) := (Extensionality A N N l k). Local step2a2 : (SUB N A) := (EQ_backwards A N l). Local step2a3 : (IN A A) := (step2a2 A step2a1). Definition naturals_main_induction2a_Out : False := (h2 step2a3). End naturals_main_induction2a. Local step2_1 : (not (EQ A N)) := naturals_main_induction2a_Out. Section naturals_main_induction2b. Hypothesis m : (IN N (Singleton A)). Local step2b1 : (EQ A N) := (Singleton_pr2 A N m). Definition naturals_main_induction2b_Out : False := (step2_1 step2b1). End naturals_main_induction2b. Local step2_2 : (not (IN N (Singleton A))) := naturals_main_induction2b_Out. Section naturals_main_induction2c. Hypothesis n: (IN N A). Local step2c1 : (StrictSUB N A) := (h1 N n). Local step2c2 : (SUB N A) := (StrictSUB_sub N A step2c1). Local step2c3 : (IN A N) := (anything_in_next_of_itself A). Local step2c4 : (IN A A) := (step2c2 A step2c3). Definition naturals_main_induction2c_Out : False := (h2 step2c4). End naturals_main_induction2c. Local step2_3 : (not (IN N A)) := naturals_main_induction2c_Out. Local step2_4 : (not (IN N N)) := (union_th3 A (Singleton A) N step2_3 step2_2). Definition naturals_main_induction2_Out : False := (step2_4 k). End naturals_main_induction2. Local sublemma1 : (not_in_itself N) := naturals_main_induction2_Out. Section naturals_main_induction3. Variable X: Ens. Hypothesis p: (IN X N). Section naturals_main_induction3em. Hypothesis contra : (not (StrictSUB X N)). Section naturals_main_induction3a. Hypothesis q: (IN X A). Local step3a1 : (StrictSUB X A) := (h1 X q). Local step3a2 : (StrictSUB X N) := (StrictSUB_trans1 X A N step3a1 sub_A_N). Definition naturals_main_induction3a_Out : False := (contra step3a2). End naturals_main_induction3a. Local step3_1 : (not (IN X A)) := naturals_main_induction3a_Out. Section naturals_main_induction3b. Hypothesis r: (IN X (Singleton A)). Local r_bis : (EQ A X) := (Singleton_pr2 A X r). Local subXA : (SUB X A) := (EQ_backwards A X r_bis). Local subAX : (SUB A X) := (EQ_forwards A X r_bis). Local step3b1 : (SUB A N) := sub_A_N. Local step3b2 : (SUB X N) := (SUB_trans X A N subXA step3b1). Section naturals_main_induction3bI. Hypothesis s: (EQ X N). Local step3bI1 : (EQ A N) := (EQ_trans A X N r_bis s). Local step3bI2 : (SUB N A) := (EQ_backwards A N step3bI1). Local step3bI3 : (IN A A):= (step3bI2 A in_A_N). Definition naturals_main_induction3bI_Out : False := (h2 step3bI3). End naturals_main_induction3bI. Local step3b3 : (not (EQ X N)) := naturals_main_induction3bI_Out. Local step3b4 : (StrictSUB X N) := (Build_StrictSUB X N step3b2 step3b3). Definition naturals_main_induction3b_Out : False := (contra step3b4). End naturals_main_induction3b. Local step3_2 : (not (IN X (Singleton A))) := naturals_main_induction3b_Out. Local step3_3 : (not (IN X N)) := (union_th3 A (Singleton A) X step3_1 step3_2). Definition naturals_main_induction3em_Out : False := (step3_3 p). End naturals_main_induction3em. Local sublemma2 : (not(not (StrictSUB X N))) := naturals_main_induction3em_Out. Definition naturals_main_induction3_Out : (StrictSUB X N) := (excluded_middle (StrictSUB X N) sublemma2). End naturals_main_induction3. Local sublemma3 : (in_then_strictsub N) := naturals_main_induction3_Out. Definition naturals_main_induction_step_Out : (naturals_main_ind_hyp N) := (Build_naturals_main_ind_hyp N sublemma3 sublemma1). End naturals_main_induction_step. Theorem naturals_main_induction_next : (A:Ens) (h: (naturals_main_ind_hyp A)) (naturals_main_ind_hyp (Next A)). Proof naturals_main_induction_step_Out. (* we have to redefine this because the inductionA statement includes the extra hypothesis (IN A Naturals) which we didn't need above so in the following formula u is forgotten ***) Theorem naturals_main_induction_next_1: (naturals_induction_nexts naturals_main_ind_hyp). Proof [A : Ens] [u: (IN A Naturals)] [h: (naturals_main_ind_hyp A)] (naturals_main_induction_next A h). Theorem naturals_main_th1: (B: Ens) (i : (IN B Naturals)) (naturals_main_ind_hyp B). Proof (naturals_inductionA naturals_main_ind_hyp naturals_main_ind_for_Zero naturals_main_induction_next_1 ). Theorem naturals_main_th2 : (B: Ens) (i: (IN B Naturals)) (in_then_strictsub B). Proof [B: Ens] [i: (IN B Naturals)] (naturals_main_ind1 B (naturals_main_th1 B i)). Theorem naturals_main_th2_rewrite : (B: Ens) (i: (IN B Naturals)) (A : Ens) (j: (IN A B)) (StrictSUB A B). Proof naturals_main_th2. Theorem naturals_main_th3 : (B: Ens) (i: (IN B Naturals)) (not_in_itself B). Proof [B: Ens] [i: (IN B Naturals)] (naturals_main_ind2 B (naturals_main_th1 B i)). Theorem naturals_main_th3_rewrite : (B: Ens) (i: (IN B Naturals)) (not (IN B B)). Proof naturals_main_th3. (******************************************************) (******************************************************) (************** FUNCTIONS *******************) (******************************************************) (******************************************************) (********** in order to bound Domain and Range we first ********) (********** define Total ***********) Definition UnionPlus := [F:Ens] (union F (Union F)). Definition Total := [R:Ens](UnionPlus (UnionPlus (UnionPlus R))). Theorem UnionPlus_th1: (X,F: Ens) (i:(IN X F)) (IN X (UnionPlus F)). Proof [X,F:Ens] [i:(IN X F)] (union_th1 F (Union F) X i). Theorem UnionPlus_th2: (X,U,F:Ens) (i:(IN X U)) (j: (IN U F)) (IN X (UnionPlus F)). Proof [X,U,F:Ens] [i:(IN X U)][j: (IN U F)] (union_th2 F (Union F) X (Union_th1 F X U i j)). Section total_th1_proof. Variables X,F: Ens. Hypothesis i: (IN X F). Remark step1 : (IN X (UnionPlus F)). Proof (UnionPlus_th1 X F i). Remark step2 : (IN X (UnionPlus (UnionPlus F))). Proof (UnionPlus_th1 X (UnionPlus F) step1). Lemma total_th1_Out : (IN X (Total F)). Proof (UnionPlus_th1 X (UnionPlus (UnionPlus F) ) step2). End total_th1_proof. Theorem Total_th1: (X,F:Ens) (i: (IN X F)) (IN X (Total F)). Proof total_th1_Out. Section total_th2_proof. Variables X,Y,F: Ens. Hypothesis i: (IN X Y). Hypothesis j: (IN Y F). Remark step1 : (IN X (UnionPlus F)). Proof (UnionPlus_th2 X Y F i j). Remark step2 : (IN X (UnionPlus (UnionPlus F))). Proof (UnionPlus_th1 X (UnionPlus F) step1). Lemma total_th2_Out : (IN X (Total F)). Proof (UnionPlus_th1 X (UnionPlus (UnionPlus F) ) step2). End total_th2_proof. Theorem Total_th2: (X,Y,F:Ens) (i: (IN X Y)) (j:(IN Y F)) (IN X (Total F)). Proof total_th2_Out. Section total_th3_proof. Variables X,Y,Z,F: Ens. Hypothesis i: (IN X Y). Hypothesis j: (IN Y Z). Hypothesis k: (IN Z F). Remark step1 : (IN Y (UnionPlus F)). Proof (UnionPlus_th2 Y Z F j k). Remark step2 : (IN X (UnionPlus (UnionPlus F))). Proof (UnionPlus_th2 X Y (UnionPlus F) i step1). Lemma total_th3_Out : (IN X (Total F)). Proof (UnionPlus_th1 X (UnionPlus (UnionPlus F)) step2). End total_th3_proof. Theorem Total_th3: (X,Y,Z,F:Ens) (i: (IN X Y)) (j:(IN Y Z)) (k: (IN Z F)) (IN X (Total F)). Proof total_th3_Out. Section total_th4_proof. Variables X,Y,Z,W,F: Ens. Hypothesis i: (IN X Y). Hypothesis j: (IN Y Z). Hypothesis k: (IN Z W). Hypothesis l: (IN W F). Remark step1 : (IN Z (UnionPlus F)). Proof (UnionPlus_th2 Z W F k l). Remark step2 : (IN Y (UnionPlus (UnionPlus F))). Proof (UnionPlus_th2 Y Z (UnionPlus F) j step1). Lemma total_th4_Out : (IN X (Total F)). Proof (UnionPlus_th2 X Y (UnionPlus (UnionPlus F)) i step2). End total_th4_proof. Theorem Total_th4: (X,Y,Z,W,F:Ens) (i: (IN X Y)) (j:(IN Y Z)) (k: (IN Z W)) (l: (IN W F)) (IN X (Total F)). Proof total_th4_Out. Section total_and_pairs_1. Variable R: Ens. Variables A,B: Ens. Hypothesis i: (IN (PAIR A B) R). Remark step1 : (IN A (First A)). Proof (Singleton_pr1 A). Remark step2 : (IN B (Singleton B)). Proof (Singleton_pr1 B). Remark step3 : (IN (Singleton B) (Second B)). Proof (Doubleton_th2 Zero (Singleton B)). Remark step4 : (IN (First A) (PAIR A B)). Proof (Doubleton_th1 (First A) (Second B)). Remark step5 : (IN (Second B) (PAIR A B)). Proof (Doubleton_th2 (First A) (Second B)). Lemma total_and_pairs_1_OutA : (IN A (Total R)). Proof (Total_th3 A (First A) (PAIR A B) R step1 step4 i). Lemma total_and_pairs_1_OutB : (IN B (Total R)). Proof (Total_th4 B (Singleton B) (Second B) (PAIR A B) R step2 step3 step5 i). End total_and_pairs_1. Theorem Relation_Total_th1 : (R: Ens) (A,B: Ens) (i: (IN (PAIR A B) R)) (IN A (Total R)). Proof total_and_pairs_1_OutA. Theorem Relation_Total_th2 : (R: Ens) (A,B: Ens) (i: (IN (PAIR A B) R)) (IN B (Total R)). Proof total_and_pairs_1_OutB. (******** ??? also prove that if m: M is a pair and M in R then PAIR_proj1 M m in Total R etc *********) (************ Domain and Range ***************) Definition Domain_prop := [R: Ens] [X:Ens] (EXISTS ([Y: Ens] (IN (PAIR X Y) R))). Definition Range_prop := [R: Ens] [Y:Ens] (EXISTS ([X: Ens] (IN (PAIR X Y) R))). (******** we use CHOICE to define evaluations ******) Definition EV := [R: Ens] [X: Ens] (CHOICE ([Y: Ens] (IN (PAIR X Y) R))). Theorem EV_pr : (R:Ens) (X: Ens) (p: (Domain_prop R X)) (IN (PAIR X (EV R X)) R). Proof [R: Ens] [X: Ens] [p: (Domain_prop R X)] (CHOICE_pr ([Y: Ens] (IN (PAIR X Y) R)) p). Definition inverse_EV := [R: Ens] [Y: Ens] (CHOICE ([X: Ens] (IN (PAIR X Y) R))). Theorem inverse_EV_pr : (R:Ens) (Y: Ens) (p: (Range_prop R Y)) (IN (PAIR (inverse_EV R Y) Y) R). Proof [R: Ens] [Y: Ens] [p: (Range_prop R Y)] (CHOICE_pr ([X: Ens] (IN (PAIR X Y) R)) p). (*********** boundedness for Domain_prop and Range_prop ******) Section Domain_prop_bounded_proof. Variable R: Ens. Local T:= (Total R). Section Domain_prop_bounded_proof_1. Variable X: Ens. Hypothesis p: (Domain_prop R X). Local Y:= (EV R X). Remark step1_1 : (IN (PAIR X Y) R). Proof (EV_pr R X p). Lemma Domain_prop_bounded_proof_1_Out : (IN X T). Proof (Relation_Total_th1 R X Y step1_1). End Domain_prop_bounded_proof_1. Remark step1 : (Bounded_By T (Domain_prop R)). Proof Domain_prop_bounded_proof_1_Out. Lemma Domain_prop_bounded_Out : (Bounded (Domain_prop R)). Proof (Bounded_th2 (Domain_prop R) T step1). End Domain_prop_bounded_proof. Theorem Domain_prop_bounded: (R: Ens) (Bounded (Domain_prop R)). Proof Domain_prop_bounded_Out. Section Range_prop_bounded_proof. Variable R: Ens. Local T:= (Total R). Section Range_prop_bounded_proof_1. Variable Y: Ens. Hypothesis p: (Range_prop R Y). Local X:= (inverse_EV R Y). Remark step1_1 : (IN (PAIR X Y) R). Proof (inverse_EV_pr R Y p). Lemma Range_prop_bounded_proof_1_Out : (IN Y T). Proof (Relation_Total_th2 R X Y step1_1). End Range_prop_bounded_proof_1. Remark step1 : (Bounded_By T (Range_prop R)). Proof Range_prop_bounded_proof_1_Out. Lemma Range_prop_bounded_Out : (Bounded (Range_prop R)). Proof (Bounded_th2 (Range_prop R) T step1). End Range_prop_bounded_proof. Theorem Range_prop_bounded: (R: Ens) (Bounded (Range_prop R)). Proof Range_prop_bounded_Out. (****** now we define domain and EV *****) Definition Domain := [R: Ens] (REPLACEMENT (Domain_prop R)). Theorem Domain_pr1 : (R: Ens) (X: Ens) (p: (Domain_prop R X)) (IN X (Domain R)). Proof [R: Ens] (REPLACEMENT_pr1 (Domain_prop R) (Domain_prop_bounded R)). Theorem Domain_pr2 : (R: Ens) (X: Ens) (i: (IN X (Domain R))) (Domain_prop R X). Proof [R: Ens] (REPLACEMENT_pr2 (Domain_prop R) (Domain_prop_bounded R)). Theorem EV_th1 : (R: Ens) (X: Ens) (i: (IN X (Domain R))) (IN (PAIR X (EV R X)) R). Proof [R: Ens] [X: Ens] [i: (IN X (Domain R))] (EV_pr R X (Domain_pr2 R X i)). Section Domain_th1_proof. Variable R: Ens. Variables X,Y: Ens. Hypothesis i: (IN (PAIR X Y) R). Remark step1 : (Domain_prop R X). Proof (EXISTS_th1 ([Y1: Ens] (IN (PAIR X Y1) R)) Y i). Lemma Domain_th1_Out : (IN X (Domain R)). Proof (Domain_pr1 R X step1). End Domain_th1_proof. Theorem Domain_th1: (R: Ens) (X,Y: Ens) (i: (IN (PAIR X Y) R)) (IN X (Domain R)). Proof Domain_th1_Out. (***** same thing for Range *********) Definition Range := [R: Ens] (REPLACEMENT (Range_prop R)). Theorem Range_pr1 : (R: Ens) (X: Ens) (p: (Range_prop R X)) (IN X (Range R)). Proof [R: Ens] (REPLACEMENT_pr1 (Range_prop R) (Range_prop_bounded R)). Theorem Range_pr2 : (R: Ens) (X: Ens) (i: (IN X (Range R))) (Range_prop R X). Proof [R: Ens] (REPLACEMENT_pr2 (Range_prop R) (Range_prop_bounded R)). Theorem inverse_EV_th1 : (R: Ens) (Y: Ens) (i: (IN Y (Range R))) (IN (PAIR (inverse_EV R Y) Y) R). Proof [R: Ens] [Y: Ens] [i: (IN Y (Range R))] (inverse_EV_pr R Y (Range_pr2 R Y i)). Section Range_th1_proof. Variable R: Ens. Variables X,Y: Ens. Hypothesis i: (IN (PAIR X Y) R). Remark step1 : (Range_prop R Y). Proof (EXISTS_th1 ([X1: Ens] (IN (PAIR X1 Y) R)) X i). Lemma Range_th1_Out : (IN Y (Range R)). Proof (Range_pr1 R Y step1). End Range_th1_proof. Theorem Range_th1: (R: Ens) (X,Y: Ens) (i: (IN (PAIR X Y) R)) (IN Y (Range R)). Proof Range_th1_Out. (******* now say EV R X is in Range R and inversely ????? *****) Section eval_in_range_proof. Variables R,X: Ens. Hypothesis i : (IN X (Domain R)). Local Y := (EV R X). Remark step1 : (IN (PAIR X Y) R). Proof (EV_th1 R X i). Lemma eval_in_range_Out : (IN Y (Range R)). Proof (Range_th1 R X Y step1). End eval_in_range_proof. Theorem EV_in_range : (R,X:Ens) (i: (IN X (Domain R))) (IN (EV R X) (Range R)). Proof eval_in_range_Out. (******) Section inv_eval_in_domain_proof. Variables R,Y: Ens. Hypothesis i : (IN Y (Range R)). Local X := (inverse_EV R Y). Remark step0 : (Range_prop R Y). Proof (Range_pr2 R Y i). Remark step1 : (IN (PAIR X Y) R). Proof (inverse_EV_pr R Y step0). Lemma inv_eval_in_domain_Out : (IN X (Domain R)). Proof (Domain_th1 R X Y step1). End inv_eval_in_domain_proof. Theorem inverse_EV_in_domain : (R,Y:Ens) (i: (IN Y (Range R))) (IN (inverse_EV R Y) (Domain R)). Proof inv_eval_in_domain_Out. (******** functions ***********) Definition is_a_relation := [R: Ens] (X: Ens) (i: (IN X R)) (is_a_pair X). Section relation_1. Variable R : Ens. Hypothesis r: (is_a_relation R). Variable S : Ens. Hypothesis h: (SUB S R). Variable X: Ens. Hypothesis i: (IN X S). Remark step1 : (IN X R). Proof (h X i). Lemma relation_1_Out : (is_a_pair X). Proof (r X step1). End relation_1. Theorem relation_sub : (R: Ens) (r: (is_a_relation R)) (S: Ens) (SUB S R) -> (is_a_relation S). Proof relation_1_Out. Definition well_definedness := [F: Ens] (X,Y,Z: Ens) (i: (IN (PAIR X Y) F)) (j: (IN (PAIR X Z) F)) (EQ Y Z). Section well_def_1. Variable F : Ens. Hypothesis w : (well_definedness F). Variable R: Ens. Hypothesis h : (SUB R F). Variables X , Y , Z : Ens. Hypothesis i: (IN (PAIR X Y) R). Hypothesis j: (IN (PAIR X Z) R). Remark step1 : (IN (PAIR X Y) F). Proof (h (PAIR X Y) i). Remark step2 : (IN (PAIR X Z) F). Proof (h (PAIR X Z) j). Lemma well_def_1_Out : (EQ Y Z). Proof (w X Y Z step1 step2). End well_def_1. Theorem well_definedness_sub : (F: Ens) (w: (well_definedness F)) (R: Ens) (h: (SUB R F)) (well_definedness R). Proof well_def_1_Out. Record is_a_function [F: Ens] : Prop := { function_is_a_relation : (is_a_relation F); function_well_definedness : (well_definedness F) }. Theorem function_sub : (F: Ens) (f: (is_a_function F)) (G: Ens) (s: (SUB G F)) (is_a_function G). Proof [F: Ens] [f: (is_a_function F)] [G: Ens] [s: (SUB G F)] (Build_is_a_function G (relation_sub F (function_is_a_relation F f) G s) (well_definedness_sub F (function_well_definedness F f) G s)). Record is_a_function_on [D,F:Ens] : Prop := { function_on_fn : (is_a_function F); function_on_dom : (EQ D (Domain F)) }. Theorem function_is_a_function_on : (F: Ens) (f: (is_a_function F)) (is_a_function_on (Domain F) F). Proof [F: Ens] [f: (is_a_function F)] (Build_is_a_function_on (Domain F) F f (EQ_refl (Domain F))). Section function_section_1. Variables F : Ens. Hypothesis f : (is_a_function F). Variables X,Y: Ens. Hypothesis i: (IN (PAIR X Y) F). Remark step1 : (IN X (Domain F)). Proof (Domain_th1 F X Y i). Local V := (EV F X). Remark step3 : (IN (PAIR X V) F). Proof (EV_th1 F X step1). Remark step5 : (well_definedness F). Proof (function_well_definedness F f). Lemma function_1_Out_F : (EQ Y V). Proof (step5 X Y V i step3). End function_section_1. Theorem function_th1: (F: Ens) (f: (is_a_function F)) (X,Y: Ens) (i : (IN (PAIR X Y) F)) (EQ Y (EV F X)). Proof function_1_Out_F. Definition Extensionally_equivalent := [F,G: Ens] (X: Ens) (i: (IN X (Domain F))) (j: (IN X (Domain G))) (EQ (EV F X) (EV G X)). Section ee_symm_proof. Variables F,G: Ens. Hypothesis e: (Extensionally_equivalent F G). Variable X : Ens. Hypothesis i: (IN X (Domain G)). Hypothesis j: (IN X (Domain F)). Remark step1 : (EQ (EV F X) (EV G X)). Proof (e X j i). Lemma ee_symm_Out : (EQ (EV G X) (EV F X)). Proof (EQ_symm (EV F X) (EV G X) step1). End ee_symm_proof. Theorem ex_eq_symm : (F,G: Ens) (Extensionally_equivalent F G)-> (Extensionally_equivalent G F). Proof ee_symm_Out. Section ee_sub_proof. Variables F,G: Ens. Hypothesis f: (is_a_function F). Hypothesis g: (is_a_function G). Hypothesis s : (SUB (Domain F) (Domain G)). Hypothesis e : (Extensionally_equivalent F G). Variable M : Ens. Hypothesis i : (IN M F). Remark step1 : (is_a_relation F). Proof (function_is_a_relation F f). Remark step2 : (is_a_pair M). Proof (step1 M i). Local X := (PR1 M). Local Y := (PR2 M). Remark step3 : (EQ M (PAIR X Y)). Proof (PAIR_proj_th1 M step2). Remark step4 : (EQ (PAIR X Y) M). Proof (EQ_symm M (PAIR X Y) step3). Remark step5 : (IN (PAIR X Y) F). Proof (Extensionality (PAIR X Y) M F step4 i). Local V := (EV F X). Remark step6 : (EQ Y V). Proof (function_th1 F f X Y step5). Remark step7 : (IN X (Domain F)). Proof (Domain_th1 F X Y step5). Remark step8 : (IN X (Domain G)). Proof (s X step7). Local W := (EV G X). Remark step9 : (EQ V W). Proof (e X step7 step8). Remark step10 : (EQ Y W). Proof (EQ_trans Y V W step6 step9). Remark step10a : (EQ W Y). Proof (EQ_symm Y W step10). Remark step11 : (IN (PAIR X W) G). Proof (EV_th1 G X step8). Remark step12 : (IN (PAIR X Y) G). Proof (Big_Extensionality ([Y1:Ens] (IN (PAIR X Y1) G)) W Y step11 step10a). Lemma ee_sub_Out : (IN M G). Proof (Extensionality M (PAIR X Y) G step3 step12). End ee_sub_proof. Theorem ex_eq_sub : (F,G: Ens) (f: (is_a_function F)) (s : (SUB (Domain F) (Domain G))) (e : (Extensionally_equivalent F G)) (SUB F G). Proof ee_sub_Out. Section ee_eq_proof. Variables F,G: Ens. Hypothesis f: (is_a_function F). Hypothesis g: (is_a_function G). Hypothesis d : (EQ (Domain F) (Domain G)). Hypothesis e : (Extensionally_equivalent F G). Remark step1 : (SUB (Domain F) (Domain G)). Proof (EQ_forwards (Domain F) (Domain G) d). Remark step2 : (SUB (Domain G) (Domain F)). Proof (EQ_backwards (Domain F) (Domain G) d). Remark step3 : (Extensionally_equivalent G F). Proof (ex_eq_symm F G e). Remark step4 : (SUB F G). Proof (ex_eq_sub F G f step1 e). Remark step5 : (SUB G F). Proof (ex_eq_sub G F g step2 step3). Lemma ee_eq_Out : (EQ F G). Proof (Build_EQ F G step4 step5). End ee_eq_proof. Theorem Extensionality_for_functions : (F,G: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (d : (EQ (Domain F) (Domain G))) (e : (Extensionally_equivalent F G)) (EQ F G). Proof ee_eq_Out. (******* evaluation ********) Section function_evaluation_proof. Variables F, X, Y: Ens. Hypothesis f : (is_a_function F). Hypothesis i : (IN (PAIR X Y) F). Local Z := (EV F X). Remark step1 : (IN X (Domain F)). Proof (Domain_th1 F X Y i). Remark step2 : (IN (PAIR X Z) F). Proof (EV_th1 F X step1). Lemma fe_Out : (EQ Y Z). Proof (function_well_definedness F f X Y Z i step2). End function_evaluation_proof. Theorem function_evaluation : (F,X,Y: Ens) (f: (is_a_function F)) (i: (IN (PAIR X Y) F)) (EQ Y (EV F X)). Proof fe_Out. (************* restricted_to ***********) Definition restricted_to := [A,F : Ens] (Set_Of F ([M : Ens] (IN (PR1 M) A))). Theorem restricted_to_th1 : (A,F : Ens) (U: Ens) (i : (IN U F)) (j: (IN (PR1 U) A)) (IN U (restricted_to A F)). Proof [A,F : Ens] [U: Ens] [i : (IN U F)] [j: (IN (PR1 U) A)] (Set_Of_th1 F ([M : Ens] (IN (PR1 M) A)) U i j). Theorem restricted_to_th2 : (A,F : Ens) (U: Ens) (i : (IN U (restricted_to A F))) (IN (PR1 U) A). Proof [A,F : Ens] [U: Ens] [i : (IN U (restricted_to A F))] (Set_Of_th2 F ([M : Ens] (IN (PR1 M) A)) U i). Theorem restricted_to_th3 : (A,F : Ens) (U: Ens) (i : (IN U (restricted_to A F))) (IN U F). Proof [A,F : Ens] [U: Ens] [i : (IN U (restricted_to A F))] (Set_Of_th3 F ([M : Ens] (IN (PR1 M) A)) U i). Theorem restricted_to_th4 : (A,F : Ens) (SUB (restricted_to A F) F). Proof [A,F: Ens] (restricted_to_th3 A F). Section restricted_to_1. Variables A,F: Ens. Section res_to_1a. Variable X : Ens. Hypothesis i : (IN X (Domain (restricted_to A F))). Local Y := (EV (restricted_to A F) X). Remark stepa1 : (IN (PAIR X Y) (restricted_to A F)). Proof (EV_th1 (restricted_to A F) X i). Remark stepa2 : (IN (PAIR X Y) F). Proof (Set_Of_th3 F ([M : Ens] (IN (PR1 M) A)) (PAIR X Y) stepa1). Local U := (PAIR X Y). Remark stepa3 : (IN (PR1 U) A). Proof (Set_Of_th2 F ([M : Ens] (IN (PR1 M) A)) U stepa1). Remark stepa4 : (EQ X (PR1 U)). Proof (PAIR_proj_th3 X Y). Remark stepa5 : (IN X A). Proof (Extensionality X (PR1 U) A stepa4 stepa3). Remark stepa6 : (IN X (Domain F)). Proof (Domain_th1 F X Y stepa2). Fact res_to_1a_Out : (IN X (intersection A (Domain F))). Proof (intersection_th3 A (Domain F) X stepa5 stepa6). End res_to_1a. Remark step1 : (SUB (Domain (restricted_to A F)) (intersection A (Domain F))). Proof res_to_1a_Out. Section res_to_1b. Variable X : Ens. Hypothesis i : (IN X (intersection A (Domain F))). Remark stepb1 : (IN X A). Proof (intersection_th1 A (Domain F) X i). Remark stepb2 : (IN X (Domain F)). Proof (intersection_th2 A (Domain F) X i). Local Y:= (EV F X). Local U := (PAIR X Y). Remark stepb3 : (IN U F). Proof (EV_th1 F X stepb2). Remark stepb4 : (EQ X (PR1 U)). Proof (PAIR_proj_th3 X Y). Remark stepb5 : (EQ (PR1 U) X). Proof (EQ_symm X (PR1 U) stepb4). Remark stepb6 : (IN (PR1 U) A). Proof (Extensionality (PR1 U) X A stepb5 stepb1). Remark stepb7 : (IN U (restricted_to A F)). Proof (restricted_to_th1 A F U stepb3 stepb6). Fact res_to_1b_Out : (IN X (Domain (restricted_to A F))). Proof (Domain_th1 (restricted_to A F) X Y stepb7). End res_to_1b. Remark step2 : (SUB (intersection A (Domain F)) (Domain (restricted_to A F))). Proof res_to_1b_Out. Lemma res_to_1_Out : (EQ (intersection A (Domain F)) (Domain (restricted_to A F))). Proof (Build_EQ (intersection A (Domain F)) (Domain (restricted_to A F)) step2 step1). End restricted_to_1. Theorem restricted_to_th5 : (A,F : Ens) (EQ (intersection A (Domain F)) (Domain (restricted_to A F)) ). Proof res_to_1_Out. Section res_to_2. Variables A,F: Ens. Hypothesis f: (is_a_function F). Hypothesis s: (SUB (Domain F) A). Variable U : Ens. Hypothesis i : (IN U F). Local X := (PR1 U). Local Y := (PR2 U). Local M := (PAIR X Y). Remark step1 : (is_a_relation F). Proof (function_is_a_relation F f). Remark step2 : (is_a_pair U). Proof (step1 U i). Remark step3 : (EQ U M). Proof (PAIR_proj_th1 U step2). Remark step4 : (EQ M U). Proof (EQ_symm U M step3). Remark step5 : (IN M F). Proof (Extensionality M U F step4 i). Remark step6 : (IN X (Domain F)). Proof (Domain_th1 F X Y step5). Remark step7 : (IN X A). Proof (s X step6). Lemma res_to_2_Out : (IN U (restricted_to A F)). Proof (restricted_to_th1 A F U i step7). End res_to_2. Theorem restricted_to_th6 : (A,F:Ens) (f: (is_a_function F)) (s: (SUB (Domain F) A)) (SUB F (restricted_to A F)). Proof res_to_2_Out. Theorem restricted_to_th7 : (A,F : Ens) (f: (is_a_function F)) (s: (SUB (Domain F) A)) (EQ F (restricted_to A F)). Proof [A,F : Ens] [f: (is_a_function F)] [s: (SUB (Domain F) A)] (Build_EQ F (restricted_to A F) (restricted_to_th6 A F f s) (restricted_to_th4 A F)). Section res_to_3. Variables A,F: Ens. Hypothesis f: (is_a_function F). Variable X: Ens. Hypothesis i: (IN X (intersection A (Domain F))). Local Y := (EV F X). Local Z := (EV (restricted_to A F) X). Remark step1 : (IN X (Domain F)). Proof (intersection_th2 A (Domain F) X i). Remark step2 : (IN X A). Proof (intersection_th1 A (Domain F) X i). Remark step3 : (EQ (intersection A (Domain F)) (Domain (restricted_to A F))). Proof (restricted_to_th5 A F). Remark step4 : (IN X (Domain (restricted_to A F))). Proof ((EQ_forwards (intersection A (Domain F)) (Domain (restricted_to A F)) step3) X i). Remark step5 : (IN (PAIR X Y) F). Proof (EV_th1 F X step1). Remark step6 : (IN (PAIR X Z) (restricted_to A F)). Proof (EV_th1 (restricted_to A F) X step4). Remark step7 : (IN (PAIR X Z) F). Proof (restricted_to_th4 A F (PAIR X Z) step6). Lemma res_to_3_Out : (EQ Y Z). Proof (function_well_definedness F f X Y Z step5 step7). End res_to_3. Theorem restricted_to_th8 : (A,F: Ens) (f: (is_a_function F)) (X: Ens) (i: (IN X (intersection A (Domain F)))) (EQ (EV F X) (EV (restricted_to A F) X)). Proof res_to_3_Out. Theorem restricted_to_th9 : (A,F: Ens) (f: (is_a_function F)) (X: Ens) (i: (IN X A)) (j : (IN X (Domain F))) (EQ (EV F X) (EV (restricted_to A F) X)). Proof [A,F: Ens] [f: (is_a_function F)] [X: Ens] [i: (IN X A)] [j : (IN X (Domain F))] (restricted_to_th8 A F f X (intersection_th3 A (Domain F) X i j)). (******** the empty function ******) Section emptyfn_1. Variable X : Ens. Hypothesis i : (IN X Zero). Remark step1 : False. Proof (EmptySet_th1 X i). Lemma emptyfn1_Out : (is_a_pair X). Proof (false_implies_everything (is_a_pair X) step1). End emptyfn_1. Theorem empty_function_relation : (is_a_relation Zero). Proof emptyfn1_Out. Section emptyfn_2. Variables X,Y,Z: Ens. Hypothesis i : (IN (PAIR X Y) Zero). Remark step1 : False. Proof (EmptySet_th1 (PAIR X Y) i). Lemma emptyfn2_Out : (EQ Y Z). Proof (false_implies_everything (EQ Y Z) step1). End emptyfn_2. Theorem empty_function_well_definedness : (well_definedness Zero). Proof [X,Y,Z: Ens] [i: (IN (PAIR X Y) Zero)] [j: (IN (PAIR X Z) Zero)] (emptyfn2_Out X Y Z i). Theorem empty_function_function : (is_a_function Zero). Proof (Build_is_a_function Zero empty_function_relation empty_function_well_definedness). Section efdom. Variable X: Ens. Hypothesis i: (IN X (Domain Zero)). Local Y := (EV Zero X). Remark step1 : (IN (PAIR X Y) Zero). Proof (EV_th1 Zero X i). Lemma efdom_Out : False. Proof (EmptySet_th1 (PAIR X Y) step1). End efdom. Theorem empty_function_domain_empty : (Its_empty (Domain Zero)). Proof efdom_Out. Theorem empty_function_domain : (EQ Zero (Domain Zero)). Proof (EQ_symm (Domain Zero) Zero (its_empty_implies_equals_emptyset (Domain Zero) empty_function_domain_empty)). (********** Cartesian product *********) Definition PowerPlus := [A : Ens] (union A (Powerset A)). Theorem PowerPlus_th1 : (A: Ens) (SUB A (PowerPlus A)). Proof [A: Ens] (union_pr1 A (Powerset A)). Theorem PowerPlus_th2 : (A: Ens) (SUB (Powerset A) (PowerPlus A)). Proof [A:Ens] (union_pr2 A (Powerset A)). Section powerplus1. Variables A,X,Y: Ens. Hypothesis x: (IN X A). Hypothesis y: (IN Y A). Local P:= (PowerPlus A). Local PP:= (PowerPlus P). Remark step1 : (IN (First X) P). Proof ((PowerPlus_th2 A) (Singleton X) (Powerset_th4 A X x)). Remark step2: (SUB P PP). Proof (PowerPlus_th1 P). Remark step3 : (IN (First X) PP). Proof (step2 (First X) step1). Remark step4: (SUB (Powerset A) P). Proof (PowerPlus_th2 A). Remark step5 : (SUB (Powerset (Powerset A)) (Powerset P)). Proof (Powerset_th7 (Powerset A) P step4). Remark step6 : (SUB (Powerset P) PP). Proof (PowerPlus_th2 P). Remark step7 : (SUB (Powerset (Powerset A)) PP). Proof (SUB_trans (Powerset (Powerset A)) (Powerset P) PP step5 step6). Remark step8 : (IN (Second Y) (Powerset (Powerset A))). Proof (Powerset_th6 A Y y). Remark step9 : (IN (Second Y) PP). Proof (step7 (Second Y) step8). Lemma powerplus1_Out : (IN (PAIR X Y) (Powerset PP)). Proof (Powerset_th5 PP (First X) (Second Y) step3 step9). End powerplus1. Definition PowerTotal := [A: Ens] (Powerset (PowerPlus (PowerPlus A))). Theorem PowerTotal_th1 : (A,X,Y: Ens) (x: (IN X A)) (y: (IN Y A)) (IN (PAIR X Y) (PowerTotal A)). Proof powerplus1_Out. Section powerplus2. Variables A,B,X,Y: Ens. Hypothesis x: (IN X A). Hypothesis y: (IN Y B). Local U:= (union A B). Remark step1: (SUB A U). Proof (union_pr1 A B). Remark step2 : (SUB B U). Proof (union_pr2 A B). Remark step3 : (IN X U). Proof (step1 X x). Remark step4 : (IN Y U). Proof (step2 Y y). Lemma powerplus2_Out : (IN (PAIR X Y) (PowerTotal U)). Proof (PowerTotal_th1 U X Y step3 step4). End powerplus2. Theorem PowerTotal_th2 : (A,B,X,Y: Ens) (x: (IN X A)) (y: (IN Y B)) (IN (PAIR X Y) (PowerTotal (union A B))). Proof powerplus2_Out. Record in_cartesian [A,B,P: Ens] : Prop := { in_cartesian_pair : (is_a_pair P); in_cartesian_pr1 : (IN (PR1 P) A); in_cartesian_pr2 : (IN (PR2 P) B) }. Section in_cartesian_bounded_proof. Variables A,B: Ens. Section cpb1. Variable U: Ens. Hypothesis i: (in_cartesian A B U). Remark step1 : (is_a_pair U). Proof (in_cartesian_pair A B U i). Local X := (PR1 U). Local Y := (PR2 U). Remark step4 : (EQ U (PAIR X Y)). Proof (PAIR_proj_th1 U step1). Remark step5 : (IN X A). Proof (in_cartesian_pr1 A B U i). Remark step6 : (IN Y B). Proof (in_cartesian_pr2 A B U i). Remark step7 : (IN (PAIR X Y) (PowerTotal (union A B))). Proof (PowerTotal_th2 A B X Y step5 step6). Lemma cpb1_Out : (IN U (PowerTotal (union A B))). Proof (Extensionality U (PAIR X Y) (PowerTotal (union A B)) step4 step7). End cpb1. Remark step8 : (Bounded_By (PowerTotal (union A B)) (in_cartesian A B)). Proof cpb1_Out. Lemma in_cartesian_bounded_Out : (Bounded (in_cartesian A B)). Proof (Bounded_th2 (in_cartesian A B) (PowerTotal (union A B)) step8). End in_cartesian_bounded_proof. Theorem in_cartesian_bounded : (A,B: Ens) (Bounded (in_cartesian A B)). Proof in_cartesian_bounded_Out. Definition Cartesian := [A,B: Ens] (REPLACEMENT (in_cartesian A B)). Theorem Cartesian_pr1 : (A,B : Ens) (M : Ens) (h: (in_cartesian A B M)) (IN M (Cartesian A B)). Proof [A,B : Ens] (REPLACEMENT_pr1 (in_cartesian A B) (in_cartesian_bounded A B)). Theorem Cartesian_pr2 : (A,B : Ens) (M : Ens) (i: (IN M (Cartesian A B))) (in_cartesian A B M). Proof [A,B : Ens] (REPLACEMENT_pr2 (in_cartesian A B) (in_cartesian_bounded A B)). Section cartesian_construction_section. Variables A,B: Ens. Variables X,Y: Ens. Hypothesis i: (IN X A). Hypothesis j: (IN Y B). Local U := (PAIR X Y). Remark step1 :(is_a_pair U). Proof (a_pair_is_a_pair X Y). Local X1 := (PR1 U). Local Y1 := (PR2 U). Remark step2 : (EQ U (PAIR X1 Y1)). Proof (PAIR_proj_th1 U step1). Remark step3 : (EQ X X1). Proof (PAIR_uni_ac X Y X1 Y1 step2). Remark step4 : (EQ Y Y1). Proof (PAIR_uni_bd X Y X1 Y1 step2). Remark step5 : (EQ X1 X) . Proof (EQ_symm X X1 step3). Remark step6 : (EQ Y1 Y) . Proof (EQ_symm Y Y1 step4). Remark step7 : (IN X1 A). Proof (Extensionality X1 X A step5 i). Remark step8 : (IN Y1 B). Proof (Extensionality Y1 Y B step6 j). Remark step9 : (in_cartesian A B U). Proof (Build_in_cartesian A B U step1 step7 step8). Lemma cartesian_construction_Out : (IN U (Cartesian A B)). Proof (Cartesian_pr1 A B U step9). End cartesian_construction_section. Theorem Cartesian_construction : (A ,B: Ens) (X,Y: Ens) (i: (IN X A)) (j: (IN Y B)) (IN (PAIR X Y) (Cartesian A B)). Proof cartesian_construction_Out. Theorem Cartesian_th1 : (A,B: Ens) (U: Ens) (i: (IN U (Cartesian A B))) (is_a_pair U). Proof [A,B,U: Ens] [i: (IN U (Cartesian A B))] (in_cartesian_pair A B U (Cartesian_pr2 A B U i)). Theorem Cartesian_proj1_th : (A,B,U: Ens) (i: (IN U (Cartesian A B))) (IN (PR1 U) A). Proof [A,B,U: Ens] [i: (IN U (Cartesian A B))] (in_cartesian_pr1 A B U (Cartesian_pr2 A B U i)). Theorem Cartesian_proj2_th : (A,B,U: Ens) (i: (IN U (Cartesian A B))) (IN (PR2 U) B). Proof [A,B,U: Ens] [i: (IN U (Cartesian A B))] (in_cartesian_pr2 A B U (Cartesian_pr2 A B U i)). Section cartpair. Variables A,B,X,Y: Ens. Hypothesis i: (IN (PAIR X Y) (Cartesian A B)). Local U:= (PAIR X Y). Local X1 := (PR1 U). Local Y1 := (PR2 U). Remark step1 : (EQ X X1). Proof (PAIR_proj_th3 X Y). Remark step2 : (IN X1 A). Proof (Cartesian_proj1_th A B U i). Lemma cartpairA_Out : (IN X A). Proof (Extensionality X X1 A step1 step2). Remark step3 : (EQ Y Y1). Proof (PAIR_proj_th4 X Y). Remark step4 : (IN Y1 B). Proof (Cartesian_proj2_th A B U i). Lemma cartpairB_Out : (IN Y B). Proof (Extensionality Y Y1 B step3 step4). End cartpair. Theorem Cartesian_pair_th1 : (A,B,X,Y: Ens) (i: (IN (PAIR X Y) (Cartesian A B))) (IN X A). Proof cartpairA_Out. Theorem Cartesian_pair_th2 : (A,B,X,Y: Ens) (i: (IN (PAIR X Y) (Cartesian A B))) (IN Y B). Proof cartpairB_Out. (********* function graphs ***********) Section relations_in_cartesian_proof. Variable R: Ens. Hypothesis r: (is_a_relation R). Local A := (Domain R). Local B := (Range R). Variable U : Ens. Hypothesis i: (IN U R). Remark step1 : (is_a_pair U). Proof (r U i). Local X := (PR1 U ). Local Y := (PR2 U ). Remark step2 : (EQ U (PAIR X Y)). Proof (PAIR_proj_th1 U step1). Remark step3 : (EQ (PAIR X Y) U). Proof (EQ_symm U (PAIR X Y) step2). Remark step4 : (IN (PAIR X Y) R). Proof (Extensionality (PAIR X Y) U R step3 i). Remark step5 : (IN X A). Proof (Domain_th1 R X Y step4). Remark step6 : (IN Y B). Proof (Range_th1 R X Y step4). Remark step7 : (IN (PAIR X Y) (Cartesian A B)). Proof (Cartesian_construction A B X Y step5 step6). Lemma relations_in_cartesian_Out : (IN U (Cartesian A B)). Proof (Extensionality U (PAIR X Y) (Cartesian A B) step2 step7). End relations_in_cartesian_proof. Theorem relations_in_cartesian : (R: Ens) (r: (is_a_relation R)) (SUB R (Cartesian (Domain R) (Range R))). Proof relations_in_cartesian_Out. Section cartesian_is_relation_proof. Variables A,B: Ens. Variable U: Ens. Variable i: (IN U (Cartesian A B)). Remark step1 : (in_cartesian A B U). Proof ( Cartesian_pr2 A B U i). Lemma cartesian_is_relation_Out : (is_a_pair U). Proof (in_cartesian_pair A B U step1). End cartesian_is_relation_proof. Theorem cartesian_is_relation : (A,B: Ens) (is_a_relation (Cartesian A B)). Proof cartesian_is_relation_Out. Theorem cartesian_subs_are_relations : (A,B: Ens) (R: Ens) (s: (SUB R (Cartesian A B))) (is_a_relation R). Proof [A,B: Ens] [R: Ens] [s: (SUB R (Cartesian A B))] (relation_sub (Cartesian A B) (cartesian_is_relation A B) R s). (******* covering ***********) Section covering_1. Variables A,B,F,G: Ens. Hypothesis f: (is_a_function F). Hypothesis g: (is_a_function G). Hypothesis u : (EQ (Domain F) (union A B)). Hypothesis v : (EQ (Domain G) (union A B)). Hypothesis i : (EQ (restricted_to A F) (restricted_to A G)). Hypothesis j : (EQ (restricted_to B F) (restricted_to B G)). Variable X : Ens. Hypothesis ix : (IN X (Domain F)). Hypothesis jx : (IN X (Domain G)). Local U := (union A B). Remark step0a : (SUB (Domain F) U). Proof (EQ_forwards (Domain F) U u). Remark iX : (IN X U). Proof (step0a X ix). Section covering_em. Hypothesis contra : (NEQ (EV F X) (EV G X)). Remark step1 : (SUB U (Domain F)). Proof (EQ_backwards (Domain F) U u). Remark step2 : (SUB U (Domain G)). Proof (EQ_backwards (Domain G) U v). Remark step3 : (SUB A (Domain F)). Proof (SUB_trans A U (Domain F) (union_pr1 A B) step1). Remark step4 : (SUB A (Domain G)). Proof (SUB_trans A U (Domain G) (union_pr1 A B) step2). Remark step5 : (SUB B (Domain F)). Proof (SUB_trans B U (Domain F) (union_pr2 A B) step1). Remark step6 : (SUB B (Domain G)). Proof (SUB_trans B U (Domain G) (union_pr2 A B) step2). Remark step7 : (IN X (Domain F)). Proof ix. Remark step8 : (IN X (Domain G)). Proof jx. Local FA := (restricted_to A F). Local FB := (restricted_to B F). Local GA := (restricted_to A G). Local GB := (restricted_to B G). Remark step9 : (EQ (EV FA X) (EV GA X)). Proof (Big_Extensionality ([fn : Ens] (EQ (EV FA X) (EV fn X))) FA GA (EQ_refl (EV FA X)) i). Remark step10 : (EQ (EV FB X) (EV GB X)). Proof (Big_Extensionality ([fn : Ens] (EQ (EV FB X) (EV fn X))) FB GB (EQ_refl (EV FB X)) j). Section covering_1_A. Hypothesis iA : (IN X A). Remark stepA1 : (EQ (EV F X) (EV FA X)). Proof (restricted_to_th9 A F f X iA step7). Remark stepA2 : (EQ (EV G X) (EV GA X)). Proof (restricted_to_th9 A G g X iA step8). Remark stepA3 : (EQ (EV GA X) (EV G X)). Proof (EQ_symm (EV G X) (EV GA X) stepA2). Remark stepA4 : (EQ (EV F X) (EV GA X)). Proof (EQ_trans (EV F X) (EV FA X) (EV GA X) stepA1 step9). Remark stepA5 : (EQ (EV F X) (EV G X)). Proof (EQ_trans (EV F X) (EV GA X) (EV G X) stepA4 stepA3). Fact stepA6 : False . Proof (contra stepA5). End covering_1_A. Remark step11 : (not (IN X A)). Proof stepA6. Section covering_1_B. Hypothesis iB : (IN X B). Remark stepB1 : (EQ (EV F X) (EV FB X)). Proof (restricted_to_th9 B F f X iB step7). Remark stepB2 : (EQ (EV G X) (EV GB X)). Proof (restricted_to_th9 B G g X iB step8). Remark stepB3 : (EQ (EV GB X) (EV G X)). Proof (EQ_symm (EV G X) (EV GB X) stepB2). Remark stepB4 : (EQ (EV F X) (EV GB X)). Proof (EQ_trans (EV F X) (EV FB X) (EV GB X) stepB1 step10). Remark stepB5 : (EQ (EV F X) (EV G X)). Proof (EQ_trans (EV F X) (EV GB X) (EV G X) stepB4 stepB3). Fact stepB6 : False . Proof (contra stepB5). End covering_1_B. Remark step12 : (not (IN X B)). Proof stepB6. Remark step13 : (not (IN X U)). Proof (union_th3 A B X step11 step12). Fact covering_em_Out : False . Proof (step13 iX). End covering_em. Lemma covering_1_Out : (EQ (EV F X) (EV G X)). Proof (excluded_middle (EQ (EV F X) (EV G X)) covering_em_Out). End covering_1. Theorem covering_th1 : (A,B,F,G: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (u : (EQ (Domain F) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (Extensionally_equivalent F G). Proof covering_1_Out. Theorem covering_th2 : (A,B,F,G: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (u : (EQ (Domain F) (union A B))) (v : (EQ (Domain G) (union A B))) (i : (EQ (restricted_to A F) (restricted_to A G))) (j : (EQ (restricted_to B F) (restricted_to B G))) (EQ F G). Proof [A,B,F,G: Ens] [f: (is_a_function F)] [g: (is_a_function G)] [u : (EQ (Domain F) (union A B))] [v : (EQ (Domain G) (union A B))] [i : (EQ (restricted_to A F) (restricted_to A G))] [j : (EQ (restricted_to B F) (restricted_to B G))] (Extensionality_for_functions F G f g (EQ_trans (Domain F) (union A B) (Domain G) u (EQ_symm (Domain G) (union A B) v)) (covering_th1 A B F G f g u i j)). (***** glueing two functions ******) Section glueing_relation_proof. Variables F,G: Ens. Hypothesis f: (is_a_relation F). Hypothesis g: (is_a_relation G). Local H:= (union F G). Variable X: Ens. Hypothesis x: (IN X H). Section gr1. Hypothesis x1: (IN X F). Lemma gr1_Out : (is_a_pair X). Proof (f X x1). End gr1. Section gr2. Hypothesis x2: (IN X G). Lemma gr2_Out : (is_a_pair X). Proof (g X x2). End gr2. Lemma gr_Out : (is_a_pair X). Proof (union_th4 (is_a_pair X) F G X x gr1_Out gr2_Out). End glueing_relation_proof. Theorem glueing_th1: (F,G: Ens) (f: (is_a_relation F)) (g: (is_a_relation G)) (is_a_relation (union F G)). Proof gr_Out. Section glueing_domain1. Variables F,G,X: Ens. Hypothesis x: (IN X (Domain (union F G))). Local Y:= (EV (union F G) X). Remark step1: (IN (PAIR X Y) (union F G)). Proof (EV_th1 (union F G) X x). Section gd1a. Hypothesis p1 : (IN (PAIR X Y) F). Remark step2 : (IN X (Domain F)). Proof (Domain_th1 F X Y p1). Lemma gd1a_Out : (IN X (union (Domain F) (Domain G))). Proof (union_th1 (Domain F) (Domain G) X step2). End gd1a. Section gd1b. Hypothesis p2: (IN (PAIR X Y) G). Remark step3 : (IN X (Domain G)). Proof (Domain_th1 G X Y p2). Lemma gd1b_Out : (IN X (union (Domain F) (Domain G))). Proof (union_th2 (Domain F) (Domain G) X step3). End gd1b. Lemma glueing_domain1_Out : (IN X (union (Domain F) (Domain G))). Proof (union_th4 (IN X (union (Domain F) (Domain G))) F G (PAIR X Y) step1 gd1a_Out gd1b_Out). End glueing_domain1. Theorem glueing_th2: (F,G: Ens) (SUB (Domain (union F G)) (union (Domain F) (Domain G))). Proof glueing_domain1_Out. Section glueing_domain2. Variables F, G, X: Ens. Hypothesis x : (IN X (union (Domain F) (Domain G))). Local H:= (union F G). Section gd2A. Hypothesis x1 : (IN X (Domain F)). Local Y := (EV F X). Remark step1 : (IN (PAIR X Y) F). Proof (EV_th1 F X x1). Remark step2 : (IN (PAIR X Y) H). Proof (union_th1 F G (PAIR X Y) step1). Lemma gd2A_Out : (IN X (Domain H)). Proof (Domain_th1 H X Y step2). End gd2A. Section gd2B. Hypothesis x1 : (IN X (Domain G)). Local Y := (EV G X). Remark step1 : (IN (PAIR X Y) G). Proof (EV_th1 G X x1). Remark step2 : (IN (PAIR X Y) H). Proof (union_th2 F G (PAIR X Y) step1). Lemma gd2B_Out : (IN X (Domain H)). Proof (Domain_th1 H X Y step2). End gd2B. Lemma gd2_Out : (IN X (Domain H)). Proof (union_th4 (IN X (Domain H)) (Domain F) (Domain G) X x gd2A_Out gd2B_Out). End glueing_domain2. Theorem glueing_th3 : (F,G: Ens) (SUB (union (Domain F) (Domain G)) (Domain (union F G))). Proof gd2_Out. Theorem glueing_th4 : (F,G: Ens) (EQ (Domain (union F G)) (union (Domain F) (Domain G))). Proof [F,G: Ens] (Build_EQ (Domain (union F G)) (union (Domain F) (Domain G)) (glueing_th2 F G) (glueing_th3 F G)). Section glueing_proof. Variables F, G: Ens. Hypothesis f: (is_a_function F). Hypothesis g: (is_a_function G). Hypothesis e: (Extensionally_equivalent F G). Local H := (union F G). Remark step1 : (is_a_relation F). Proof (function_is_a_relation F f). Remark step2 : (is_a_relation G). Proof (function_is_a_relation G g). Remark step3 : (well_definedness F). Proof (function_well_definedness F f). Remark step4 : (well_definedness G). Proof (function_well_definedness G g). Remark step5 : (is_a_relation H). Proof (glueing_th1 F G step1 step2). Section glu_wd. Variables X,Y,Z: Ens. Hypothesis i: (IN (PAIR X Y) H). Hypothesis j: (IN (PAIR X Z) H). Section gluA. Hypothesis j1 : (IN (PAIR X Z) F). Hypothesis i1 : (IN (PAIR X Y) F). Lemma gluA_Out : (EQ Y Z). Proof (step3 X Y Z i1 j1). End gluA. Section gluB. Hypothesis j1 : (IN (PAIR X Z) G). Hypothesis i1 : (IN (PAIR X Y) F). Remark Bstep1 : (IN X (Domain F)). Proof (Domain_th1 F X Y i1). Remark Bstep2 : (IN X (Domain G)). Proof (Domain_th1 G X Z j1). Remark Bstep3 : (EQ Y (EV F X)). Proof (function_th1 F f X Y i1). Remark Bstep4 : (EQ Z (EV G X)). Proof (function_th1 G g X Z j1). Remark Bstep5 : (EQ (EV G X) Z). Proof (EQ_symm Z (EV G X) Bstep4). Remark Bstep6 : (EQ (EV F X) (EV G X)). Proof (e X Bstep1 Bstep2). Remark Bstep7 : (EQ Y (EV G X)). Proof (EQ_trans Y (EV F X) (EV G X) Bstep3 Bstep6). Lemma gluB_Out : (EQ Y Z). Proof (EQ_trans Y (EV G X) Z Bstep7 Bstep5). End gluB. Section gluC. Hypothesis j1 : (IN (PAIR X Z) F). Hypothesis i1 : (IN (PAIR X Y) G). Remark Cstep1 : (IN X (Domain F)). Proof (Domain_th1 F X Z j1). Remark Cstep2 : (IN X (Domain G)). Proof (Domain_th1 G X Y i1). Remark Cstep3 : (EQ Y (EV G X)). Proof (function_th1 G g X Y i1). Remark Cstep4 : (EQ Z (EV F X)). Proof (function_th1 F f X Z j1). Remark Cstep5 : (EQ (EV F X) Z). Proof (EQ_symm Z (EV F X) Cstep4). Remark Cstep6 : (EQ (EV F X) (EV G X)). Proof (e X Cstep1 Cstep2). Remark Cstep6a: (EQ (EV G X) (EV F X)). Proof (EQ_symm (EV F X) (EV G X) Cstep6). Remark Cstep7 : (EQ Y (EV F X)). Proof (EQ_trans Y (EV G X) (EV F X) Cstep3 Cstep6a). Lemma gluC_Out : (EQ Y Z). Proof (EQ_trans Y (EV F X) Z Cstep7 Cstep5). End gluC. Section gluD. Hypothesis j1 : (IN (PAIR X Z) G). Hypothesis i1 : (IN (PAIR X Y) G). Lemma gluD_Out : (EQ Y Z). Proof (step4 X Y Z i1 j1). End gluD. Remark step6 : (IN (PAIR X Y) F) -> (EQ Y Z). Proof (union_th4 ((IN (PAIR X Y) F) -> (EQ Y Z)) F G (PAIR X Z) j gluA_Out gluB_Out). Remark step7 : (IN (PAIR X Y) G) -> (EQ Y Z). Proof (union_th4 ((IN (PAIR X Y) G) -> (EQ Y Z)) F G (PAIR X Z) j gluC_Out gluD_Out). Lemma glu_wd_Out : (EQ Y Z). Proof (union_th4 (EQ Y Z) F G (PAIR X Y) i step6 step7). End glu_wd. Remark step8 : (well_definedness H). Proof glu_wd_Out. Lemma glueing_proof_Out : (is_a_function H). Proof (Build_is_a_function H step5 step8). End glueing_proof. Theorem glueing_th5 : (F, G: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (e: (Extensionally_equivalent F G)) (is_a_function (union F G)). Proof glueing_proof_Out. (********** composition ********) Record Comp_inter [F,G,X,Y,Z: Ens] : Prop := { Comp_inter_xy : (IN (PAIR X Y) F); Comp_inter_yz : (IN (PAIR Y Z) G) }. Record Comp_prop [F,G,X: Ens] : Prop := { Comp_pair : (is_a_pair X); Comp_intern : (EXISTS ([Y: Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))) }. Definition Comp_INTER := [F,G,X: Ens] (CHOICE ([Y: Ens] (Comp_inter F G (PR1 X) Y (PR2 X)))). Theorem Comp_INTER_pr1 : (F,G,X: Ens) (c: (Comp_prop F G X)) (Comp_inter F G (PR1 X) (Comp_INTER F G X) (PR2 X)). Proof [F,G,X: Ens] [c: (Comp_prop F G X)] (CHOICE_pr ([Y: Ens] (Comp_inter F G (PR1 X) Y (PR2 X))) (Comp_intern F G X c)). Theorem Comp_INTER_th1 : (F,G,X: Ens) (c: (Comp_prop F G X)) (IN (PAIR (PR1 X) (Comp_INTER F G X)) F). Proof [F,G,X: Ens] [c: (Comp_prop F G X)] (Comp_inter_xy F G (PR1 X) (Comp_INTER F G X) (PR2 X) (Comp_INTER_pr1 F G X c)). Theorem Comp_INTER_th2 : (F,G,X: Ens) (c: (Comp_prop F G X)) (IN (PAIR (Comp_INTER F G X) (PR2 X)) G). Proof [F,G,X: Ens] [c: (Comp_prop F G X)] (Comp_inter_yz F G (PR1 X) (Comp_INTER F G X) (PR2 X) (Comp_INTER_pr1 F G X c)). Theorem Comp_prop_th1 : (F,G,X: Ens) (c: (Comp_prop F G X)) (IN (PR1 X) (Domain F)). Proof [F,G,X: Ens] [c: (Comp_prop F G X)] (Domain_th1 F (PR1 X) (Comp_INTER F G X) (Comp_INTER_th1 F G X c)). Theorem Comp_prop_th2 : (F,G,X: Ens) (c: (Comp_prop F G X)) (IN (PR2 X) (Range G)). Proof [F,G,X: Ens] [c: (Comp_prop F G X)] (Range_th1 G (Comp_INTER F G X) (PR2 X) (Comp_INTER_th2 F G X c)). Section comp_prop_3. Variables F,G,X: Ens. Hypothesis c: (Comp_prop F G X). Remark step1 : (is_a_pair X). Proof (Comp_pair F G X c). Remark step2 : (IN (PR1 X) (Domain F)). Proof (Comp_prop_th1 F G X c). Remark step3 : (IN (PR2 X) (Range G)). Proof (Comp_prop_th2 F G X c). Remark step4 : (in_cartesian (Domain F) (Range G) X). Proof (Build_in_cartesian (Domain F) (Range G) X step1 step2 step3). Lemma comp_prop_3_Out : (IN X (Cartesian (Domain F) (Range G))). Proof (Cartesian_pr1 (Domain F) (Range G) X step4). End comp_prop_3. Theorem Comp_prop_th3 : (F,G,X: Ens) (c: (Comp_prop F G X)) (IN X (Cartesian (Domain F) (Range G))). Proof comp_prop_3_Out. Theorem composition_bounded_by : (F,G: Ens) (Bounded_By (Cartesian (Domain F) (Range G)) (Comp_prop F G)). Proof Comp_prop_th3. Theorem composition_bounded : (F,G: Ens) (Bounded (Comp_prop F G)). Proof [F,G: Ens] (Bounded_th2 (Comp_prop F G) (Cartesian (Domain F) (Range G)) (composition_bounded_by F G)). Definition COMP := [F,G: Ens] (REPLACEMENT (Comp_prop F G)). (******* note that this is the full composition of relations, like composition of correspondences in algebraic geometry ************) Theorem COMP_pr1 : (F,G,X: Ens) (Comp_prop F G X) -> (IN X (COMP F G)). Proof [F,G,X: Ens] (REPLACEMENT_pr1 (Comp_prop F G) (composition_bounded F G) X). Theorem COMP_pr2 : (F,G,X: Ens) (IN X (COMP F G)) -> (Comp_prop F G X). Proof [F,G,X: Ens] (REPLACEMENT_pr2 (Comp_prop F G) (composition_bounded F G) X). Theorem COMP_th1 : (F,G: Ens) (is_a_relation (COMP F G)). Proof [F,G,X: Ens] [i: (IN X (COMP F G))] (Comp_pair F G X (COMP_pr2 F G X i)). Theorem COMP_th2: (F,G: Ens) (SUB (COMP F G) (Cartesian (Domain F) (Range G))). Proof [F,G,X: Ens] [i: (IN X (COMP F G))] (Comp_prop_th3 F G X (COMP_pr2 F G X i)). Theorem COMP_th3 : (F,G,X: Ens) (i: (IN X (COMP F G))) (IN (PAIR (PR1 X) (Comp_INTER F G X)) F). Proof [F,G,X: Ens] [i: (IN X (COMP F G))] (Comp_INTER_th1 F G X (COMP_pr2 F G X i)). Theorem COMP_th4 : (F,G,X: Ens) (i: (IN X (COMP F G))) (IN (PAIR (Comp_INTER F G X) (PR2 X)) G). Proof [F,G,X: Ens] [i: (IN X (COMP F G))] (Comp_INTER_th2 F G X (COMP_pr2 F G X i)). Definition Comp_INTERp := [F,G,X,Y: Ens] (Comp_INTER F G (PAIR X Y)). Section COMPp. Variables F,G,X,Y: Ens. Hypothesis i: (IN (PAIR X Y) (COMP F G)). Local Z:= (PAIR X Y). Remark step1 : (IN Z (COMP F G)). Proof i. Remark step2 : (EQ X (PR1 Z)). Proof (PAIR_proj_th3 X Y). Remark step3 : (EQ Y (PR2 Z)). Proof (PAIR_proj_th4 X Y). Remark step4 : (IN (PAIR (PR1 Z) (Comp_INTERp F G X Y)) F). Proof (COMP_th3 F G Z step1). Remark step5 : (IN (PAIR (Comp_INTERp F G X Y) (PR2 Z)) G). Proof (COMP_th4 F G Z step1). Lemma COMPp_Out3 : (IN (PAIR X (Comp_INTERp F G X Y)) F). Proof (Substitute X (PR1 Z) ([U: Ens] (IN (PAIR U (Comp_INTERp F G X Y)) F)) step2 step4). Lemma COMPp_Out4: (IN (PAIR (Comp_INTERp F G X Y) Y) G). Proof (Substitute Y (PR2 Z) ([U: Ens] (IN (PAIR (Comp_INTERp F G X Y) U ) G)) step3 step5). End COMPp. Theorem COMP_th3p : (F,G,X,Y: Ens) (i: (IN (PAIR X Y) (COMP F G))) (IN (PAIR X (Comp_INTERp F G X Y)) F). Proof COMPp_Out3. Theorem COMP_th4p : (F,G,X,Y: Ens) (i: (IN (PAIR X Y) (COMP F G))) (IN (PAIR (Comp_INTERp F G X Y) Y) G). Proof COMPp_Out4. Section comp_wd. Variables F,G: Ens. Hypothesis f: (well_definedness F). Hypothesis g: (well_definedness G). Variables X, Y, Z: Ens. Hypothesis i: (IN (PAIR X Y) (COMP F G)). Hypothesis j: (IN (PAIR X Z) (COMP F G)). Local V := (Comp_INTERp F G X Y). Local W := (Comp_INTERp F G X Z). Remark step1 : (IN (PAIR X V) F). Proof (COMP_th3p F G X Y i). Remark step2 : (IN (PAIR V Y) G). Proof (COMP_th4p F G X Y i). Remark step3 : (IN (PAIR X W) F). Proof (COMP_th3p F G X Z j). Remark step4 : (IN (PAIR W Z) G). Proof (COMP_th4p F G X Z j). Remark step5: (EQ V W). Proof (f X V W step1 step3). Remark step6: (IN (PAIR V Z) G). Proof (Substitute V W ([U: Ens](IN (PAIR U Z) G)) step5 step4). Lemma comp_wd_Out : (EQ Y Z). Proof (g V Y Z step2 step6). End comp_wd. Theorem composition_well_definedness : (F,G: Ens) (f: (well_definedness F)) (g: (well_definedness G)) (well_definedness (COMP F G)). Proof comp_wd_Out. Theorem composition_th1: (F,G: Ens) (f: (well_definedness F)) (g: (well_definedness G)) (is_a_function (COMP F G)). Proof [F,G: Ens] [f: (well_definedness F)] [g: (well_definedness G)] (Build_is_a_function (COMP F G) (COMP_th1 F G) (composition_well_definedness F G f g)). Theorem composition_th2: (F,G: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (is_a_function (COMP F G)). Proof [F,G: Ens] [f: (is_a_function F)] [g: (is_a_function G)] (composition_th1 F G (function_well_definedness F f) (function_well_definedness G g)). Section comp_ev_1. Variables F,G,X,Y,Z: Ens. Hypothesis i: (IN (PAIR X Y) F). Hypothesis j: (IN (PAIR Y Z) G). Remark step1 : (Comp_inter F G X Y Z). Proof (Build_Comp_inter F G X Y Z i j). Local W := (PAIR X Z). Remark step2 : (EQ X (PR1 W)). Proof (PAIR_proj_th3 X Z). Remark step3 : (EQ (PR1 W) X). Proof (EQ_symm X (PR1 W) step2). Remark step4 : (EQ Z (PR2 W)). Proof (PAIR_proj_th4 X Z). Remark step5 : (EQ (PR2 W) Z). Proof (EQ_symm Z (PR2 W) step4). Remark step6 : (Comp_inter F G X Y (PR2 W)). Proof (Substitute (PR2 W) Z ([U: Ens] (Comp_inter F G X Y U)) step5 step1). Remark step7 : (Comp_inter F G (PR1 W) Y (PR2 W)). Proof (Substitute (PR1 W) X ([U: Ens] (Comp_inter F G U Y (PR2 W))) step3 step6). Remark step8 : (EXISTS ([Y1: Ens] (Comp_inter F G (PR1 W) Y1 (PR2 W)))). Proof (EXISTS_th1 ([Y1: Ens] (Comp_inter F G (PR1 W) Y1 (PR2 W))) Y step7). Remark step9 : (Comp_prop F G W). Proof (Build_Comp_prop F G W (a_pair_is_a_pair X Z) step8). Lemma comp_ev_1_Out : (IN W (COMP F G)). Proof (COMP_pr1 F G W step9). End comp_ev_1. Theorem COMP_th5 : (F,G,X,Y,Z: Ens) (i: (IN (PAIR X Y) F)) (j: (IN (PAIR Y Z) G)) (IN (PAIR X Z) (COMP F G)). Proof comp_ev_1_Out. Section comp_ev_2. Variables F,G,X: Ens. Hypothesis i: (IN X (Domain F)). Hypothesis j: (IN (EV F X) (Domain G)). Local Y:= (EV F X). Local Z:= (EV G Y). Remark step1 : (IN (PAIR X Y) F). Proof (EV_th1 F X i). Remark step2 : (IN (PAIR Y Z) G). Proof (EV_th1 G Y j). Lemma comp_ev_2_Out : (IN (PAIR X Z) (COMP F G)). Proof (COMP_th5 F G X Y Z step1 step2). End comp_ev_2. Theorem composition_th3: (F,G,X: Ens) (i: (IN X (Domain F))) (j: (IN (EV F X) (Domain G))) (IN (PAIR X (EV G (EV F X))) (COMP F G)). Proof comp_ev_2_Out. Section comp_ev_3. Variables F,G,X: Ens. Hypothesis f: (is_a_function F). Hypothesis g: (is_a_function G). Hypothesis i: (IN X (Domain F)). Hypothesis j: (IN (EV F X) (Domain G)). Local Z := (EV G (EV F X)). Local W := (EV (COMP F G) X). Remark step1 : (is_a_function (COMP F G)). Proof (composition_th2 F G f g). Remark step2 : (well_definedness (COMP F G)). Proof (function_well_definedness (COMP F G) step1). Remark step3 : (IN (PAIR X Z) (COMP F G)). Proof (composition_th3 F G X i j). Remark step4 : (IN X (Domain (COMP F G))). Proof (Domain_th1 (COMP F G) X Z step3). Remark step5 : (IN (PAIR X W) (COMP F G)). Proof (EV_th1 (COMP F G) X step4). Lemma comp_ev_3_Out: (EQ W Z). Proof (step2 X W Z step5 step3). End comp_ev_3. Theorem composition_th4: (F,G,X: Ens) (f: (is_a_function F)) (g: (is_a_function G)) (i: (IN X (Domain F))) (j: (IN (EV F X) (Domain G))) (EQ (EV (COMP F G) X) (EV G (EV F X))). Proof comp_ev_3_Out. (******** associativity of composition ********) Section comp_assoc_1. Variables F,G,H,P: Ens. Hypothesis p: (IN P (COMP F (COMP G H))). Remark step1 : (is_a_pair P). Proof (COMP_th1 F (COMP G H) P p). Local X:= (PR1 P). Local W:= (PR2 P). Local Y := (Comp_INTERp F (COMP G H) X W). Local Z := (Comp_INTERp G H Y W). Remark step2 : (EQ P (PAIR X W)). Proof (PAIR_proj_th1 P step1). Remark step3 : (EQ (PAIR X W) P). Proof (EQ_symm P (PAIR X W) step2). Remark step4 : (IN (PAIR X W) (COMP F (COMP G H))). Proof (Substitute (PAIR X W) P ([U: Ens] (IN U (COMP F (COMP G H)))) step3 p). Remark step5 : (IN (PAIR X Y) F). Proof (COMP_th3p F (COMP G H) X W step4). Remark step6 : (IN (PAIR Y W) (COMP G H)). Proof (COMP_th4p F (COMP G H) X W step4). Remark step7 : (IN (PAIR Y Z) G). Proof (COMP_th3p G H Y W step6). Remark step8 : (IN (PAIR Z W) H). Proof (COMP_th4p G H Y W step6). Remark step9: (IN (PAIR X Z) (COMP F G)). Proof (COMP_th5 F G X Y Z step5 step7). Remark step10 : (IN (PAIR X W) (COMP (COMP F G) H)). Proof (COMP_th5 (COMP F G) H X Z W step9 step8). Lemma comp_assoc_1_Out : (IN P (COMP (COMP F G) H)). Proof (Substitute P (PAIR X W) ([U: Ens] (IN U (COMP (COMP F G) H))) step2 step10). End comp_assoc_1. Theorem COMP_assoc_th1: (F,G,H: Ens) (SUB (COMP F (COMP G H)) (COMP (COMP F G) H)). Proof comp_assoc_1_Out. Section comp_assoc_2. Variables F,G,H,P: Ens. Hypothesis p: (IN P (COMP (COMP F G) H )). Remark step1 : (is_a_pair P). Proof (COMP_th1 (COMP F G) H P p). Local X:= (PR1 P). Local W:= (PR2 P). Local Z := (Comp_INTERp (COMP F G) H X W). Local Y := (Comp_INTERp F G X Z). Remark step2 : (EQ P (PAIR X W)). Proof (PAIR_proj_th1 P step1). Remark step3 : (EQ (PAIR X W) P). Proof (EQ_symm P (PAIR X W) step2). Remark step4 : (IN (PAIR X W) (COMP (COMP F G) H) ). Proof (Substitute (PAIR X W) P ([U: Ens] (IN U (COMP (COMP F G) H) )) step3 p). Remark step5 : (IN (PAIR X Z) (COMP F G)). Proof (COMP_th3p (COMP F G) H X W step4). Remark step6 : (IN (PAIR Z W) H). Proof (COMP_th4p (COMP F G) H X W step4). Remark step7 : (IN (PAIR X Y) F). Proof (COMP_th3p F G X Z step5). Remark step8 : (IN (PAIR Y Z) G). Proof (COMP_th4p F G X Z step5). Remark step9: (IN (PAIR Y W) (COMP G H)). Proof (COMP_th5 G H Y Z W step8 step6). Remark step10 : (IN (PAIR X W) (COMP F (COMP G H)) ). Proof (COMP_th5 F (COMP G H) X Y W step7 step9). Lemma comp_assoc_2_Out : (IN P (COMP F (COMP G H)) ). Proof (Substitute P (PAIR X W) ([U: Ens] (IN U (COMP F (COMP G H)))) step2 step10). End comp_assoc_2. Theorem COMP_assoc_th2: (F,G,H: Ens) (SUB (COMP (COMP F G) H) (COMP F (COMP G H))). Proof comp_assoc_2_Out. Theorem COMP_assoc : (F,G,H: Ens) (EQ (COMP F (COMP G H)) (COMP (COMP F G) H)). Proof [F,G,H: Ens] (Build_EQ (COMP F (COMP G H)) (COMP (COMP F G) H) (COMP_assoc_th1 F G H) (COMP_assoc_th2 F G H)). (**** one should also do the identity function of a set, and show that composition with it is the same as restriction to the set etc. ****) (***** } \end{document} %*)