\input utility.tdf
%\input logic.tdf
%\input sets.tdf
%\input logic.test
\input common.tdf 
\vskip 1in 

\centerline{\bigrm Common Notions}
\vskip .5in 

{\bigrm
This file contains propositions 
at a level which ordinarily causes them
to be accepted without explicit justification. 
The purpose of this file is to serve as a
repository of such results which may be explicitly referred to in
checkable proofs.
In most cases these propositions assert what most people
regard as trivialities.  In some cases they represent
familiar facts of set theory.  There are also however propositions which
will strike the reader unaccustomed to working with non-denoting terms as obscure.  
Further, there
is a development of an unconventional way dealing with familiar expressions
such as `$(x < y)$', and `$(x + y)$' which is intended to do away with
common so-called abuses of notation without sacrificing the readability
of basic mathematical notation.}

{\bigrm
When renumbering this file, use it as the first argument
to renum and then add an argument for every other file which depends on this
file.}



\vfill\eject

\chap{1. Logic}
\lineb

\noindent{}Sentence Logic

The sentence logic is standard.  There are the following forms:

%primitive_formula:  \Not\pvar
%
$\Not \pvar$;  The negation of $\pvar$.

$(\pvar \c \qvar)$; If $\pvar$ then $\qvar$.

$(\pvar \Iff \qvar)$;  $\pvar$ if and only if $\qvar$.

$(\pvar \And \qvar)$;  $\pvar$ and $\qvar$.

$(\pvar \Or \qvar)$;  $\pvar$ or $\qvar$.

$\true$; The Boolean constant for ``true.''

$\false$; The Boolean constant for ``false.''
\lineb

\noindent{Other Definitions}

\noindent{}Dichotomy, Trichotomy, etc.

$((\pvar \Onr \qvar )\Iff ((\pvar \And \Not\qvar)
\Or (\Not\pvar \And \qvar)))$

$((\pvar \Onr \qvar \Onr \rvar) \Iff ((\pvar \And \Not(\qvar \Or \rvar))
\Or (\Not\pvar \And(\qvar \Onr \rvar))))$
\lineb

\noindent{\bf{Predicate Logic}}

A full exposition of the predicate logic
can be found in {\it Notre Dame Journal of Formal Logic}, Vol. 22, Num. 3.
It can be interpreted as ordinary logic with a single null object adjoined
which serves the referent for non-denoting terms.  The null object
lies outside the range of quantification. 
\lineb

%primitive_term: \an x \pbar x

\noindent{}Primitives

`$\an x \pbar x$' denotes an object satisfying the predicate $\pbar x$ if such
an object exists.  If no such object exists it is a non-denoting term.  
In the denoting case it is the same as the Hilbert epsilon symbol used 
by Bourbaki and discussed by Sierpinski for example on page 93 of his
book {\it Ordinal and Cardinal Numbers}.  

'$(x = y)$'  is ordinary equality.  It means that both `$x$' and `$y$' denote
the same object.  In particular it means that both terms are denoting terms.

'$(x \ident y)$' means that $x$ and $y$ are identical.  This means that 
the terms `$x$' and `$y$' are substitutionally equivalent.  It is used
to define terms, but its use is not restricted to definitions.
It does not imply
existence.
\lineb


\noindent{}Definitions

\prop 1.1 $(\ex x \Iff (x = x))$

\prop 1.2 $(\Some x \pbar x \Iff \ex \an x \pbar x)$

\prop 1.3 $(\Each x \pbar x \Iff \Not \Some x \Not \pbar x)$

\prop 1.4 $(\The x \pbar x \ident \an y \Each x(\pbar x \Iff x = y))$

\prop 1.5  $(\One x \pbar x \Iff \ex \The x \pbar x)$ 

\prop 1.6  $(\Unq x \pbar x \Iff (\Some x \pbar x \c \One x \pbar x))$

\prop 1.7 $(\Nul \ident \an x \false)$
\lineb


\noindent{}Axioms

\prop 1.8 $(x \ident y \c (\pbar x \c \pbar y))$

\prop 1.9 $(x=y \c x \ident y)$

\Prop 1.10 $(y = \an x \pbar x \c \pbar y)$

\Prop 1.11 $(\ex y  \c (\pbar y \c \Some x \pbar x))$

\Prop 1.12 $(\Each x (\pbar x \Iff \qbar x) \c \an x \pbar x \ident \an x \qbar x)$

\Prop 1.13 $(y \ident \an x (x = y))$
\lineb


\noindent{}Theorems of Identity

\Prop 1.14 $(x \ident x)$

\Prop 1.15 $(x \ident y \c y \ident x)$

\Prop 1.16 $(x \ident y\And y \ident z \c x \ident z)$

\Prop 1.17 $(x \ident y\c \pbar x \Iff \pbar y)$

\Prop 1.18 $(x \ident y\c \ubar x \ident \ubar y)$
\lineb


\noindent{}Theorems of Equality

\Prop 1.19 $(x = y \c y = x)$

\Prop 1.20 $(x = y \Iff y = x)$

\Prop 1.21 $(x = y\And y = z \c x = z)$

\Prop 1.22 $(y = x\And y = z \c x = z)$

\Prop 1.23 $(x \ident y \And y = z \c x = z)$

\Prop 1.24 $(x = y \And y \ident z \c x = z)$

\Prop 1.25 $(x = y \c \pbar x \Iff \pbar y)$

\Prop 1.26 $(x = y \c \ubar x \ident \ubar y)$
\lineb

\noindent{}Theorems of the Existence Predicate
 
\Prop 1.27 $(x = y \c \ex x)$

\Prop 1.28 $(x = y \c \ex y)$

\Prop 1.29 $(\ex x \c x = x)$

\Prop 1.30 $(x \ident y \And \ex y \c x =y)$

\Prop 1.31 $(x \ident y \And \ex x \c x =y)$

\Prop 1.32 $((\ex x \c x = y) \And (\ex y \c x = y) \c x \ident y)$

\Prop 1.33 $((\ex x \Iff \ex y) \And (\ex x \c x = y) \c x \ident y)$

\Prop 1.34 $((\ex x \Or \ex y \c x = y) \c x \ident y)$

\Prop 1.35 $ \Not \ex \Nul$

\lineb

\noindent{}Theorems of Quantification

Most inferences based on quantification rules are handled by rules of
inference and only seldom need explicit reference.  A few that have been
needed explicitly are listed here.

\Prop 1.36 $(\Some y (\pvar  \And \pbar y) \Iff \pvar \And \Some y \pbar y)$

\Prop 1.37 $(\One x(\pvar\And\rbar x)\Iff \pvar\And\One x\rbar x)$
\lineb

\noindent{}Theorems of Quantification and Existence

\Prop 1.38 $\Each x \ex x$

\Prop 1.39 $(\Some y (y = x) \Iff \ex x)$

\Prop 1.40 $(\ex x \Iff \Some y (x = y) )$

\Prop 1.41 $(\ex x \Iff \Some y (y = x))$ 

\Prop 1.42 $(\Some y (x = y) \Iff \ex x)$

\Prop 1.43 $(\ex x \And \pbar x \Iff \Some y(y = x \And \pbar y))$

\lineb

\noindent{\bf Indefinite Descriptions} 

Indefinite descriptions are used often in assignment statements
in proofs, especially in the presence of existence quantifiers.
\lineb

\Prop 1.44 $(y \ident \an x \pbar x \c \ex y \Iff \Some x \pbar x )$

\Prop 1.45 $(y \ident \an x \pbar x \And \Some x \pbar x \c \pbar y)$
\lineb


\chap{2.  The Conditional Operator}

\noindent{}Definitions

\prop 2.1 $((\pvar \cond a )\ident \an x (\pvar \And x = a))$

\prop 2.2 $((\pvar \cond a \els b)\ident \an x ((\pvar \And x = a)\Or (\Not\pvar \And x = b)))$
\lineb

 The expression `$(\pvar \cond x)$' may be read ``if $\pvar$ then $x$.''
This is a conditional expression whose semantic
(not syntactic) validity is contingent on
the truth of $\pvar$.
When this conditional operator is used in a definition
it makes the existence of the defined object 
contingent on stated conditions.   A definition of the form
$(y \ident (\pvar \cond x))$ defines $y$ as the object $x$ provided
that $\pvar$ is true.  Otherwise `$y$' is non-denoting, or ``undefined.''
It provides
a straightforward mechanism for handling the common practice of preceding
definitions by ``let'' conditions.\footnote*{Suppes [1972], p18, discusses
such definitions and provides another mechanism which is pragmatic
but unsatisfying.}  
The following properties characterize the
conditional operator.
\lineb

\noindent{}Theorems

\prop 2.3 $(\pvar \c (\pvar \cond x) \ident x)$

\prop 2.4 $(\ex (\pvar \cond x) \Iff \pvar \And \ex x)$

\prop 2.5 $(y = (\pvar \cond x) \Iff \pvar \And y = x)$

\prop 2.6 $(\pvar \Iff \qvar \c (\pvar \cond x) \ident (\qvar \cond x))$

\prop 2.7 $((\pvar \c a \ident b)\c (\pvar \cond a) \ident (\pvar \cond b))$
\lineb


It is often, although not always,
the case that satisfaction of the condition $\pvar$ ensures existence
of the conditioned term $x$. The following two lemmas describe this 
situation. 
\lineb

\prop 2.8 $((\pvar \c \ex x) \c (\ex (\pvar \cond x) \Iff \pvar))$

\prop 2.9 $((\pvar \c \ex x) \c 
	(\pvar \Iff (\pvar \cond x) = x))$
	\lineb

Because definitions encapsulate a complete characterization of
a concept they are generally ponderous and unwieldy as 
inference tools, the best of which are succint little implications
and identities.
Experience shows that theorems whose sole
purpose is to break definitions down into manageable pieces
are of great value in expediting inferences.
Such theorems will be referred to as unwrapping theorems.


For definitions having the simple form $(y \ident (\pvar \cond x))$ 
we have several unwrapping theorems:
\lineb

\Prop 2.10 $(y \ident (\pvar \cond x) \And \pvar \c y \ident x)$

\Prop 2.11 $(y \ident (\pvar \cond x) \c \ex y \Iff \pvar \And \ex x)$

\Prop 2.12 $(y \ident (\pvar \cond x) \And \ex x \c \ex y \Iff \pvar )$

\Prop 2.13 $(y \ident (\pvar \cond x) \c \ex y \Iff \pvar \And y = x)$

\Prop 2.14 $(y \ident (\pvar \cond x) \And \ex y \c  y = x)$

\Prop 2.15 $(y \ident (\pvar \cond x) \And (\pvar \c \ex x)
	\c \ex y \Iff \pvar)$

\Prop 2.16 $(y \ident (\pvar \cond x) \And (\pvar \c \ex x)
	\c y = x \Iff \pvar) $

\Prop 2.17 $(y \ident (\pvar \cond x)
	\c z = y \Iff \pvar \And z = x) $
	\lineb

In some conditional definitions, the conditioned object is always
known to exist.  In this case the following may be useful:
	\lineb

\Prop 2.18 $((y \ident (\pvar \cond x)) \And \ex x \c \ex y \Iff \pvar)$

\Prop 2.19 $((y \ident (\pvar \cond x)) \And \ex x \c y = x \Iff \pvar)$
	\lineb

\noindent{\bf Conditional with an Else}
\lineb

Because the precedence of the two operators in 
the expression `$(\pvar \cond x \els y)$' are equal it
is not automatically parsed as either `$((\pvar \cond x) \els y)$'
or  `$(\pvar \cond (x \els y))$'.

\Prop 2.20 $(\ex (\pvar \cond x \els y) \Iff (\pvar \And \ex x) \Or(\Not\pvar \And\ex y))$

\Prop 2.21 $(z \ident (\pvar \cond x \els y) \c \ex z \Iff (\pvar \And \ex x)\Or (\Not\pvar \And \ex y))$

\Prop 2.22 $(\Not \pvar  \c (\pvar \cond x \els y) \ident y)$

\Prop 2.23 $(\pvar  \c (\pvar \cond x \els y) \ident x)$

\Prop 2.24 $(\pvar \And \ex x \c (\pvar \cond x \els y) = x)$

\Prop 2.25 $(\Not \pvar \And \ex y \c (\pvar \cond x \els y) = y)$

\Prop 2.26 $(\pvar \And z \ident (\pvar \cond x \els y) \c z \ident x)$

\Prop 2.27 $(\Not \pvar \And z \ident (\pvar \cond x \els y) \c z \ident y)$

\Prop 2.28 $(\pvar \And z \ident (\pvar \cond x \els y) \And \ex x \c z = x)$

\Prop 2.29 $(\Not\pvar \And z \ident (\pvar \cond x \els y) \And \ex y \c z = y)$
\lineb



\chap{3. Definite Descriptions} 

`$\The x \pbar x$' stands for the object $x$ such that $\pbar x$.  
There are two quantifiers closely related to the definite description.
We write `$\One x \pbar x$' to mean that there is exactly one $x$ such that $\pbar x$ and
we write `$\Unq x \pbar x$' to mean that there is at most one $x$ such that $\pbar x$. 
 Some first properties of the definite description are:
\lineb

\noindent{Definitions} 

\prop 3.1 $(\The x \pbar x \ident \an y \Each x(\pbar x \Iff x = y))$

\prop 3.6 $(\The \ubar x \ls x;\pbar x\rs \ident \The t \Some x;\pbar x (t = \ubar x))$ 

\prop 3.7 $(\The \ubarp xy \ls x,y;\pbarp xy\rs \ident \The t \Some x,y;\pbarp xy (t = \ubarp xy))$ 

\lineb

\noindent{Theorems} 

\prop 3.8 $(\ex \The x \pbar x \Iff \One x \pbar x)$

\prop 3.9 $(y = \The x \pbar x \Iff \Unq x \pbar x \And \pbar y \And \ex y)$

\Prop 3.10 $(y= \The x \pbar x \c \pbar y)$

\Prop 3.11 $(y =\The x\pbar x \And \pbar z \And \ex z \c z=y)$

\Prop 3.12 $(y = \The \ubar x \ls x = a \rs
\Iff \ex a \And y = \ubar a)$

\Prop 3.13 $(y = a 
\c \ubar y \ident \The \ubar x \ls x = a \rs)$

\Prop 3.14 $(\One x \pbar x \c 
y = \The x\pbar x\Iff\pbar y\And \ex y)$
\lineb


The bare definite description occurs often in assignment statements in proofs.
The following are useful unwrapping theorems:
\lineb

\Prop 3.15 $(y \ident \The x \pbar x \And
\One x \pbar x \c z = y \Iff \pbar z \And \ex z)$

\Prop 3.16 $(y \ident \The x \pbar x \And
\One x \pbar x \And \Not \pbar \Nul \c
 z = y \Iff \pbar z )$

\Prop 3.17 $(y \ident \The x\pbar x \And \One x\pbar x \c \pbar y)$

\Prop 3.18 $(y \ident \The \ubar x\ls x = a\rs \And z = a \c y \ident \ubar z)$

\lineb

\chap{4. Conditionals and Cases}

It is occasionally useful to include cases in definitions.  An ``else''
operator is used for this purpose.  The expression $(x \els y)$ denotes
$x$ provided that $x$ exists,  else it is the same as $y$. 

 A case operator which is like the else operator but symmetric with respect
to its arguments is the operator in the expression `$(x \case y)$'.  This
expression denotes whichever of $x$ and $y$ exists.  If both exist then they
must agree. 
\lineb

\noindent{Definitions} 

\prop 3.2 $((x \case y) \ident \The t (t = x \Or t = y))$

\prop 3.3 $(\Case x;\pbar x \ubar x \ident \The t \Some x;\pbar x(t = \ubar x))$

%\prop 3.4 $(\Case x,y \ubarp xy \ident \The t \Some x,y(t = \ubarp xy))$

\prop 3.5 $((x \els y) \ident \The t (t = x \Or (\Not \ex x \And t = y)))$

\lineb

\noindent{Theorems} 

\prop 4.1 $(\ex(x \case y) \Iff (\ex x \Iff \Not \ex y)\Or x = y)$

\prop 4.2 $(\ex(x \case y) \Iff (x \case y)= x \Or (x \case y)= y)$

\prop 4.3 $(z\ident (x\case y) \Iff z = x = y \Or (z = x \And \Not\ex y
) \Or (z = y \And \Not \ex x) \Or \Not \ex z)$

\prop 4.4 $(z = (x\case y) \Iff z = x = y \Or (z = x \And \Not\ex y
) \Or (z = y \And \Not \ex x) )$

\prop 4.5 $(\Not(\ex x \And \ex y) \c z = (x\case y) \Iff z = x \Or z = y)$

\prop 4.6 $(\Not(\ex x \And \ex y) \c \ex (x\case y) \Iff \ex x \Or \ex y)$

\prop 4.7 $(\ex(x \els y \els z) \Iff \ex x \Or \ex y \Or \ex z)$

\prop 4.8 $(\ex ((\pvar \cond x) \els y) \Iff (\pvar \And \ex x) \Or \ex y)$

\prop 4.9 $(\pvar \And \ex x \c ((\pvar \cond x )\els y) = x)$

\Prop 4.10 $(\pvar \And z \ident ((\pvar \cond x )\els y) \And \ex x \c z = x)$

\Prop 4.11 $(\Not \pvar \And z \ident ((\pvar \cond x )\els y) \c z \ident y)$

\Prop 4.12 $(\Not \pvar \Or \Not \ex x \c ((\pvar \cond x) \els y) \ident y)$

\Prop 4.13 $(z \ident ((\pvar \cond x) \els y) \c \ex z \Iff (\pvar \And \ex x)\Or \ex y)$
\lineb

\chap{5. Conditionals and Definite Descriptions}

In definitions the definite description usually occurs in a conditioned form.
Unwrapping theorems which are useful in these contexts follow:
	\lineb

\prop 5.1 $(y \ident(\pvar \cond\The x\pbar x)
\c \ex y \Iff \pvar \And \One x\pbar x)$

\prop 5.2 $(y \ident(\pvar \cond\The x\pbar x)
\And (\pvar \c \One x\pbar x)
\c \ex y \Iff \pvar )$

\prop 5.3 $(y \ident (\pvar \cond \The x\pbar x) \And
	(\pvar \c \One x \pbar x) 
	\c (\pvar \c x = y \Iff \pbar x \And \ex x)) $

\prop 5.4 $(y \ident (\pvar \cond \The x\pbar x) \And
	(\pvar \c \ex \The x \pbar x) 
	\c (x = y \Iff \pvar \And \pbar x \And \ex x)) $

\prop 5.5 $(y \ident (\pvar \cond \The x\pbar x) \And
	(\pvar \c \One x \pbar x) 
	\c (x = y \Iff \pvar \And \pbar x \And \ex x)) $

\prop 5.6 $(y = (\pvar \cond \The x \pbar x) \Iff \pvar \And y = \The x \pbar x)$
	\lineb



\chap{6. Logic Facts involving Negated Predicates}
	\lineb

6.1 and 6.2 and related items are listed in a section on logic because
they answer a question stemming from the acceptance of non-denoting 
terms  in the language,  namely what  does it mean to use a non-denoting
term in a mathematical statement.  In English non-denoting terms can
be syncategorematic expressions which play a useful role in spite
of their non-denoting status,  the words `everything', `something', and `nothing'
being noteworthy examples of this.  With non-denoting terms in mathematics,
nothing would prohibit a statement such as ``nothing belongs to $x$'' from being a true
statement of the form $(y \in x)$ with $x$ empty and
with $y$ being a non-denoting term playing the role of the word ``nothing.''
6.1 and 6.2 rule this sort of thing out.   They say nothing about elementhood
itself
and thus do not belong as axioms of set theory.  
	\lineb


 


\noindent{}Semantic Axioms

\prop 6.1 $(x \in y \c \ex x)$

\prop 6.2 $(x \in y \c \ex y)$
	\lineb

\noindent{}Definitions of Negated Predicates

Since the logical negation $\Not(x \in y)$ cannot have the semantic property asserted
by 6.1 and 6.2 it is useful to have  a negative form which does.  The same
is true of equality.  Subsequent slashed operators are defined
in the same way.
	\lineb


\prop 6.3 $((x \notin y) \Iff (\ex x \And \ex y \And \Not (x \in y)))$

\prop 6.4 $((x \ne y) \Iff  (\ex x \And \ex y \And \Not (x = y)))$
	\lineb

\noindent{}Theorems

\prop 6.5 $(x \in y \And x \notin y \c \false)$

\prop 6.6 $(\ex x \And \ex y \And \Not(x \in y)\c x\notin y)$

\prop 6.7 $(\ex x \And \ex y \And \Not(x \in y) \c x \notin y)$

\prop 6.8 $(\ex x \And \ex y \c \Not(x \in y) \Iff x \notin y)$

\prop 6.9 $(\ex x \And \ex y \c \Not(x \notin y) \Iff x \in y)$

\Prop 6.10 $(x \notin y \c \Not(x \in y))$

\Prop 6.11 $(a \in c \And b \notin c \c a \ne b)$

\Prop 6.12 $(a \in c \And b \notin c \c b \ne a)$

\Prop 6.13 $(a \in b \And a \notin c \c b \ne c)$

\Prop 6.14 $(a \in b \And a \notin c \c c \ne b)$

\Prop 6.15 $(x = y \And x \ne y \c \false)$

\Prop 6.16 $(x \ne x \c \false)$

\Prop 6.17 $(\ex x \And \ex y \And \Not(x = y)\c x\ne y)$

\Prop 6.18 $(x \ne y \c \ex x \And \ex y \And \Not(x = y))$

\Prop 6.19 $(x \ne y \c \ex x)$

\Prop 6.20 $(x \ne y \c \ex y)$

\Prop 6.21 $(x \ne y \c \Not(x = y))$

\Prop 6.22 $(\ex x \And \ex y \And \Not(x\ne y)\c x=y)$

\Prop 6.23 $(x = y \c \Not(x \ne y))$

\Prop 6.24 $(\ex x \And \ex y \c \Not(x = y)\Iff x\ne y)$

\Prop 6.25 $(x \ne y \c y \ne x)$

\Prop 6.26 $(x \ne y \Iff y \ne x)$

\Prop 6.27 $(\ex x \And \ex y \c x = y \Or x \ne y)$

\lineb


\vfill\eject
\chap{7. Set Theory}

The set theory is Morse-Kelley set theory formulated in the above logic.
It needs no axiom of choice because the logic already contains a stronger axiom.
\lineb  

\noindent{\bf Primitive Formula}

The sole primitive formula is `$(x \in y)$', meaning that $x$ belongs to $y$.
\lineb  

\noindent{\bf Definitions}

\noparse\noindent{}The set of $x$ such that $\pbar x$ is written `$\setof x \pbar x$':  

\prop 7.1 $(\setof x \pbar x \ident 
\The y\Each x (x \in y \Iff \pbar x \And \Some z (x \in z)))$

\noindent{}The universe: 

\prop 7.2 $(\U \ident \setof x \true)$

\noindent{}The empty set: 

\prop 7.3 $(\e \ident \setof x \false)$

\noindent{}Inclusion:

\prop 7.4 $((a \i b) \Iff (\ex a \And \ex b \And \Each x (x \in a \c x \in b)))$

\noindent{}The power set:

\prop 7.5 $(\sb x \ident (\ex x \cond \setof y (y \i x)))$

\noindent{}The singleton:

\prop 7.6 $(\{x\} \ident (x \in \U \cond \setof y (y = x)))$ 
\lineb

\noindent{\bf Axioms}

\noindent{Classification Axiom}

\prop 7.7 $\ex \setof x \pbar x$
\lineb


\noindent{Subset Axiom}

\prop 7.8 $(x \i y \in \U \c x \in \U)$
\lineb

\noindent{Power Set Axiom}

\prop 7.9 $(x \in \U \c \sb x \in \U)$
\lineb

\noindent{Axiom of Regularity}

\Prop 7.10 $(x \ne \e \c \Not \Each y \in x \Some z \in x (z \in y))$
\lineb

\noindent{Axiom of Replacement}

\Prop 7.11 $(y \in \U \And \Each x \in y (\ubar x \in \U)
\c \setof z \Some x \in y(z = \ubar x) \in \U)$
\lineb

\noindent{Axiom of Infinity}

\Prop 7.12 $\Some y \in \U (\e \in y \And \Each x \in y(\{x\} \in y))$
\lineb

\noindent{Non-Vacuity Axiom}

This axiom may be used instead of the axiom of infinity if 
only finite sets are to be postulated. 

\Prop 7.13 $(\U \ne \e)$
\lineb

\noindent{\bf{ Classifier Theorems}}	

\Prop 7.14 $(y \in \setof x \pbar x \Iff \pbar y \And y \in \U)$

\Prop 7.15 $(y \in \setof x \pbar x \c \pbar y)$

\Prop 7.16 $(\Each x( \pbar x \c \qbar x) \c \setof x \pbar x \i \setof x \qbar x)$

\Prop 7.17 $(\Each x( \pbar x \Iff \qbar x) \c \setof x \pbar x = \setof x \qbar x)$

\Prop 7.18 $(\Each x;\pbar x( \qbar x \Iff \rbar x) \c \setof x;\pbar x\qbar x = \setof x ;\pbar x \rbar x)$

\Prop 7.19 $(\ex A \And \Each x (\pbar x \Iff  x \in A) \c \setof x \pbar x = A)$

\Prop 7.20 $(\ex A \And \Each x (x\in A \Iff \qbar x) \c  A = \setof x \qbar x)$

\Prop 7.21 $(\ex A \Iff \setof x (x \in A) = A)$

\Prop 7.22 $(\ex A \Iff \setof x \ls x \in A \rs = A)$
\lineb
\lineb

\chap{8. Classifier Unwrapping Theorems}	

A bare bones definition using the classifier has the form $(y \ident \setof x \pbar x)$.
For such definitions we have these unwrapping theorems:
\lineb

\prop 8.1 $(y \ident \setof x \pbar x \Iff y = \setof x \pbar x)$

\prop 8.2 $(y \ident \setof x \pbar x \c \ex y)$

\prop 8.3 $(y \ident \setof x \pbar x \c x \in y \Iff \pbar x \And x \in \U)$
	\lineb

In 8.3 the requirement that $(x \in \U)$ is needed to avoid the Russell
paradox.  The following two theorems are useful in facilitating the
checking of this requirement.     
	\lineb

\prop 8.4 $(y \ident \setof x \pbar x \And \Each x(\pbar x \c x \in \U)
	\c x \in y \Iff \pbar x \And \ex x)$

\prop 8.5 $(y \ident \setof x \pbar x \And \Each x(\pbar x \c x \in \U)
	\And \Not \pbar \Nul \c x \in y \Iff \pbar x)$
	\lineb



The ``definition'' being unwrapped may also be an assignment statement in the proof 
of a theorem and
the enabling ``theorem'' would in this case be a previous note.  The classifier has
several syntactic variants.  Unwrapping theorems for a few more
are as follows: 
\lineb 
 
\prop 8.6 $(y \ident \setof x \in A\pbar x
	\c x \in y \Iff x\in A \And \pbar x)$

\prop 8.7 $(y \ident \setof x \in A \pbar x \And \ex A \c y \i A)$

\prop 8.8 $(y \ident \setof \ubar x \ls x ;\pbar x\rs
	\c z \in y \Iff \Some x ;\pbar x(z=\ubar x)\And z \in \U)$

\prop 8.9 $(y \ident \setof \ubar x \ls x ;\pbar x\rs \c \ex y )$

\Prop 8.10 $(y \ident \setof \ubar x \ls x ;\pbar x\rs \And
	\Each x ;\pbar x(\ubar x \in \U)
	\c z \in y \Iff \Some x ;\pbar x(z=\ubar x))$

\Prop 8.11 $(y\ident \setof \ubarp xy 
\ls x ,y ;\pbarp xy\rs \And
\Each x  \Each y ( \pbarp xy \c \ubarp xy \in \U) \c $
 $z \in y \Iff \Some x  \Some y;\pbarp xy (z = \ubarp xy ))$

\Prop 8.12 $(y\ident \setof \ubarp xy 
\ls x,y, \in A;\pbarp xy\rs \c \ex y) $

\Prop 8.13 $(y\ident \setof \ubarp xy 
\ls x,y, \in A;\pbarp xy\rs \And \Each x,y,\in A(\pbarp xy \c \ubarp xy \in \U)\c $
 $z \in y \Iff \Some x,y, \in A(\pbarp xy \And z = \ubarp xy ))$
\lineb




\noindent{\bf Conditionals and the Classifier}

 The conditioned classifier is probably the most commonly occurring form
on the right sides of definitions.  It is appropriate therefore to
list many variations: 
	\lineb

\Prop 8.14 $(y \ident (\pvar \cond \setof x \pbar x) 
		\c \ex y \Iff \pvar)$

\Prop 8.15 $(y \ident (\pvar \cond \setof x \pbar x) 
		\c  y = \setof x \pbar x \Iff \pvar)$

\Prop 8.16 $(y \ident (\pvar \cond \setof x \pbar x) 
		\c z = y \Iff \pvar \And z = \setof x \pbar x)$

\Prop 8.17 $(y \ident (\pvar \cond \setof x \pbar x)
\c z \in y \Iff \pvar \And z \in \U \And \pbar z)$

\Prop 8.18 $(y \ident (\pvar \cond \setof x \pbar x) 
	 \And \Each x(\pbar x \c x \in \U)
	\c z \in y \Iff \pvar \And \pbar z \And \ex z)$

\Prop 8.19 $(y \ident (\pvar \cond \setof x \pbar x) \And 
	\Each x(\pbar x \c x \in \U) \And \Not \pbar \Nul 
	\c z \in y \Iff \pvar \And \pbar z)$

\Prop 8.20 $(y \ident (\pvar \cond \setof x \pbar x) \And 
	(\pvar \c \Each x(\pbar x \c x \in \U)) \And \Not \pbar \Nul 
	\c z \in y \Iff \pvar \And \pbar z)$

\Prop 8.21 $(y \ident (\pvar \cond \setof x \in A\pbar x)
\c x \in y \Iff \pvar \And x \in A \And \pbar x)$

\Prop 8.22 $(y \ident (\pvar \cond\setof x \in A\pbar x)
\c \ex y \Iff \pvar)$


\Prop 8.23 $(y \ident (\pvar \cond \setof x \i A \pbar x)
\c \ex y \Iff \pvar)$

\Prop 8.24 $(y \ident (\pvar \cond \setof x \i A \pbar x)
\And (\pvar \c A \in \U) \c z \in y \Iff 
\pvar \And z \i A \And \pbar z)$


\Prop 8.25 $(y \ident(\pvar\cond\setof\ubar x \ls x;\pbar x\rs)
\c z \in y\Iff\pvar\And\Some x;\pbar x(z=\ubar x)\And z \in \U)$

\Prop 8.26 $(y \ident (\pvar \cond 
\setof \ubar x \ls x\in A\rs) \c \ex y\Iff\pvar)$

\Prop 8.27 $(y \ident (\pvar \cond \setof \ubar x \ls x;\pbar x\rs) \And
	\Each x;\pbar x(\ubar x \in \U)
	\c z \in y \Iff \pvar \And \Some x;\pbar x(z=\ubar x))$

\Prop 8.28 $(y\ident (\pvar \cond \setof \ubarp xy 
\ls x,y;\pbarp xy\rs) \c \ex y \Iff \pvar)$

\Prop 8.29 $(y\ident (\pvar \cond\setof \ubarp xy 
\ls x,y;\pbarp xy\rs) \c $
 $z \in y \Iff \pvar\And 
\Some x,y(\pbarp xy \And z = \ubarp xy \And z \in \U))$

\Prop 8.30 $(y\ident (\pvar \cond\setof \ubarp xy 
\ls x,y, \in A;\pbarp xy\rs) \c $
 $z \in y \Iff \pvar\And 
\Some x,y, \in A(\pbarp xy \And z = \ubarp xy )\And z \in \U)$

\Prop 8.31 $(y\ident (\pvar \cond\setof \ubarp xy 
\ls x ,y ;\pbarp xy\rs) \And
\Each x  \Each y ( \pbarp xy \c \ubarp xy \in \U) \c $
\lineb $z \in y \Iff \pvar\And 
\Some x  \Some y;\pbarp xy (z = \ubarp xy ))$

\Prop 8.32 $(y\ident (\pvar \cond\setof \ubarp xy 
\ls x \in w,y \in \ubar x;\pbarp xy\rs) \And
\Each x  \Each y (x \in w \And y \in \ubar x \And \pbarp xy \c \ubarp xy \in \U) \c $
\lineb $z \in y \Iff \pvar\And 
\Some x \in w \Some y\in \ubar x;\pbarp xy (z = \ubarp xy ))$
	\lineb



\chap{9. The Empty Set and the Universe}

\noindent{Recall definitions}

\noindent{}7.3 $(\e \ident \setof x \false)$

\noindent{}7.2 $(\U \ident \setof x \true)$

\noindent{Theorems}

\prop 9.1 $\ex \e$

\prop 9.2 $(a \in b \c b \ne \e)$

\prop 9.3 $\Not(x \in \e)$

\prop 9.4 $(x \in \e \Iff \false)$

\prop 9.5 $(a \in b \And c = \e \c a \notin c)$

\prop 9.6 $(b \ne \e \Iff \Some x (x \in b))$

\prop 9.7 $(\Some x (x \in b)\c b \ne \e )$

\prop 9.8 $(b \ne \e \c \Some x (x \in b))$

\prop 9.9 $(b = \e \Iff \Each x (x \notin b))$

\Prop 9.10 $(\ex A \And \Each x \Not(x \in A)\c A= \e)$

\Prop 9.11 $(A = \e \c \Each x \in A \pbar x)$

\Prop 9.12 $\Each x \in \e \pbar x$

\Prop 9.13 $(\e = \setof x \false)$

\Prop 9.14 $(\setof x \false = \e)$

\Prop 9.15 $(\Not\pvar \c \setof x \pvar  = \e)$

\Prop 9.16 $(\setof x \pbar x \ne \e \Iff \Some x \pbar x)$

\Prop 9.17 $(\Each x \Not\pbar x \c \setof x \pbar x = \e)$

\Prop 9.18 $\ex \U$

\Prop 9.19 $(\e \in \U)$

\Prop 9.20 $(x \in A \c x \in \U)$

\Prop 9.21 $(\setof x \ex x = \U)$

\Prop 9.22 $(\ex x \c x = \e \Or x \ne \e)$

\Prop 9.23 $(\ex x \c \Not (x = \e) \Iff x \ne \e)$

\Prop 9.24 $(\ex x \c \Not (x \ne \e) \Iff x = \e)$

\Prop 9.25 $(A \ne \e \And x \ident \an y(y\in A)\c x\in A)$
\lineb

\chap{10. Complementation}	

\noindent{Definition}

\prop 10.1 $(\Cmpl A \ident (\ex A \cond \setof x \Not(x \in A)))$

\noindent{Theorems}

\prop 10.2 $(\ex \Cmpl A \Iff \ex A)$

\prop 10.3 $(\Cmpl \Cmpl A  \ident A)$

\prop 10.4 $(x \in \Cmpl y \c \Not(x \in y))$

\prop 10.5 $(x \in \U \And \ex y \c \Not(x \in \Cmpl y) \Iff x \in y)$

\prop 10.6 $(x \in \U \And \ex y \c x \in y \Iff \Not(x \in \Cmpl y))$

\prop 10.7 $(x \in \U \And \ex y \And \Not(x \in \Cmpl y) \c x \in y)$

\prop 10.8 $(x \in \U \And \ex y \And \Not(x \in y) \c x \in \Cmpl y)$

\prop 10.9 $(x \in y \c \Not(x \in \Cmpl y))$

\Prop 10.10 $(x \in y \And x \in \Cmpl y\c \false)$

\lineb

\chap{11. Inclusion}	

\noindent{Recall definition}

\noindent{}7.4 $((a \i b) \Iff (\ex a \And \ex b \And \Each x (x \in a \c x \in b)))$

\noindent{Theorems}

\prop 11.1 $(A \i B \c \ex A)$

\prop 11.2 $(A \i B \c \ex B)$

\prop 11.3 $(A \i B \c \ex A \And \ex B)$

\prop 11.4 $(\ex A \And \ex B \c A \i B \Iff \Each x (x \in A \c x \in B))$

\prop 11.5 $(\ex A \And \ex B \c \Not(A \i B) \Iff \Some x (x \in A \And \Not(x \in B)))$

\prop 11.6 $(\ex A \And \ex B \And \Each x(x \in A\c x\in B) \c A \i B)$

\prop 11.7 $(x \in A \And A \i B \c x \in B)$

\prop 11.8 $(x \in y \And \Not(x \in z) \And y \i z \c \false)$

\prop 11.9 $(x \notin B \And A \i B \c x \notin A)$

\Prop 11.10 $(A \i B \And B \i C \c A \i C)$

\Prop 11.11 $(A \i B \And B \i A \Iff A = B)$

\Prop 11.12 $(A = B \Iff \ex A \And \ex B \And \Each x (x \in A \Iff x \in B))$

\Prop 11.13 $(A \i B \And B \i A \c A = B)$

\Prop 11.14 $(A = B \c A \i B)$

\Prop 11.15 $(A = B \c B \i A)$

\Prop 11.16 $(\ex A \c A \i A)$

\Prop 11.161 $(\ex A \Iff A \i A)$

\Prop 11.17  $(x,y,\in A \And A \i B \c x,y,\in B)$

\Prop 11.18 $(A\i B \And \Each x \in B \pbar x\c\Each x\in A\pbar x)$

\Prop 11.19 $(A\ne\e \And A \i B \c B\ne\e)$

\Prop 11.20 $(\e \i A \Iff \ex A)$

\Prop 11.21 $(A \i \e \Iff A = \e)$

\Prop 11.22 $(A \i \e \c A = \e)$

\Prop 11.23 $(\U \i A \c A = \U)$

\Prop 11.24 $(\U \i A \Iff A = \U)$

\Prop 11.25$(A \i B \And B \in \U \c A\in \U)$

\Prop 11.26 $(A \i \U \c \ex A)$

\Prop 11.27 $(\ex A\c A \i \U )$

\Prop 11.28 $(A \i \U \Iff \ex A)$

\Prop 11.29 $(A \i B \c \setof x \in A \pbar x \i \setof x \in B \pbar x)$

\Prop 11.30 $(A \i B \c \setof x \i A \pbar x \i \setof x \i B \pbar x)$

\Prop 11.31 $(A \i B \c \Cmpl B \i \Cmpl A)$

\Prop 11.32 $(A \i \Cmpl B \c B \i \Cmpl A)$

\Prop 11.33 $(\Cmpl A \i B \c \Cmpl B  \i A)$

\Prop 11.34 $(\Cmpl A \i \Cmpl B \c B \i A)$

\Prop 11.35 $(A \i B \Iff \Cmpl B \i \Cmpl A)$

\Prop 11.36 $(A \i \Cmpl B \Iff B \i \Cmpl A)$

\Prop 11.37 $(\Cmpl A \i B \Iff \Cmpl B  \i A)$

\Prop 11.38 $(\Cmpl A \i \Cmpl B \Iff B \i A)$

\Prop 11.39 $(A\i B \And \One x \in B \pbar x \And \Some x\in A
\pbar x \c \One x \in A \pbar x)$
\lineb

\chap{12.  Proper Inclusion}	

\noindent{Definition}

\prop 12.1 $((A \i \ne B) \Iff (A \i B \And A \ne B))$

\noindent{Theorems}

\prop 12.2 $(A \i \ne B \c A \i B \And A \ne B)$

\prop 12.3 $(A \i \ne B \c A \i B)$

\prop 12.4 $(A \i \ne B \c A \ne B)$

\prop 12.5 $(A \i \ne B \c \Not(A = B))$

\prop 12.6 $(A \i B \And \Not(A = B) \c A \i \ne B)$

\prop 12.7 $(A \i B \And \Not(B = A) \c A \i \ne B)$

\prop 12.8 $(A \i \ne B \c \Some x \in B(x \notin A))$
\lineb

\chap{13.  Pairwise Intersections}

\noindent{Definition}

\prop 13.1 $((A \cap B) \ident (\ex A \And \ex B \cond \setof x(x \in A \And x \in B)))$

\noindent{Theorems}

\prop 13.2 $(\ex (A \cap B) \Iff \ex A \And \ex B)$

\prop 13.3 $(x \in A \cap B \Iff x \in A \And x \in B)$

\prop 13.4 $(x \in A \And x \in B \c x \in A \cap B)$

\prop 13.5 $(x \in A \cap B \c x \in A)$

\prop 13.6 $(x \in A \cap B \c x \in B)$

\prop 13.7 $(A \cap B \ident B \cap A)$

\prop 13.8 $(A \cap A \ident A)$

\prop 13.9 $((A \cap B) \cap C \ident A \cap (B\cap C))$

\Prop 13.10 $(A\cap (B \cap C) \ident (A \cap B) \cap C)$

\Prop 13.11 $(A \cap B = \e \And x \in A \c x \notin B)$

\Prop 13.12 $(A \cap B = \e \And x \in B \c x \notin A)$

\Prop 13.13 $(A \cap B = \e \And x \in A \c x \in \Cmpl B)$

\Prop 13.14 $(A \cap B = \e \And x \in B \c x \in \Cmpl A)$

\Prop 13.15 $(\ex A \And B \i C \c A \cap B\i A\cap  C)$

\Prop 13.16 $(\ex A \And B \i C \c B \cap A\i C\cap  A)$

\Prop 13.17 $(A\i B \And \ex C\c A\cap C \i B\cap C)$

\Prop 13.18 $(A \i B \And A \i C \c A \i B \cap C)$

\Prop 13.19 $(A \i C \And B \i D \c A \cap B \i C \cap D)$

\Prop 13.20 $(A\i B \Iff A\cap B = A)$

\Prop 13.21 $(A\i B \Iff B\cap A = A)$

\Prop 13.22 $(A\i B \Iff A = A\cap B )$

\Prop 13.23 $(A\i B \Iff A = B\cap A )$

\Prop 13.24 $(C = A \cap B \c  C \i A)$

\Prop 13.25 $(C = A \cap B \c  C \i B)$

\Prop 13.26 $(\ex(A\cap B) \c A\cap B \i A)$

\Prop 13.27 $(\ex(A\cap B) \c A\cap B\i B)$

\Prop 13.28 $(\ex(A\cap B) \c A\cap B\i A \And A \cap B \i B)$

\Prop 13.29 $(\ex A \And \ex B \c A\cap B \i A)$

\Prop 13.30 $(\ex A\And \ex B \c A\cap B\i B)$

\Prop 13.31 $(A\cap B \ne \e \c A \ne \e)$

\Prop 13.32 $(A \cap B \ne \e \c B \ne \e)$

\Prop 13.33 $(\ex A \c A\cap \e = \e)$

\Prop 13.34 $(\ex A \c \e\cap A = \e)$

\Prop 13.35 $(\ex A \c A \cap \Cmpl A = \e)$

\Prop 13.36 $(\ex A \c \Cmpl A \cap A = \e)$

\Prop 13.37 $(A \cap \U \ident A)$

\Prop 13.38 $(\U \cap A \ident A)$

\Prop 13.39 $(A \in \U \And B \in \U \c A \cap B \in \U)$

\Prop 13.40 $(\setof x \pbar x \cap \setof x \qbar x = \setof x (\pbar x\And\qbar x))$

\Prop 13.41 $( \setof x (\pbar x\And\qbar x) = \setof x \pbar x \cap \setof x \qbar x)$
\lineb

\chap{14. Ternary Intersections}	

\noindent{Definition}

\prop 14.1 $((A\cap B \cap C )\ident ((A \cap B) \cap C))$

\noindent{Theorems}

\prop 14.2 $(x \in A \cap B \cap C \Iff x \in A \And x \in B\And x \in C)$

\prop 14.3 $(A\cap B \cap C \ident A \cap (B \cap C))$

\prop 14.4 $((A\cap B) \cap C \ident A \cap B \cap C)$

\prop 14.5 $(A\cap (B \cap C) \ident A \cap B \cap C)$

\prop 14.6 $(A \cap B \cap C \ne \e \c A \cap B \ne \e)$

\prop 14.7 $(A \cap B \cap C \ne \e \c B \cap C \ne \e)$
\lineb


\chap{15. Pairwise Unions}

\noindent{Definition}

\prop 15.1 $((A \cup B) \ident (\ex A \And \ex B \cond \setof x(x \in A \Or x \in B)))$

\noindent{Theorems}

\prop 15.2 $(\ex (A \cup B) \Iff \ex A \And \ex B)$

\prop 15.3 $(A \cup B \in \U \Iff A \in \U \And B \in \U)$

\prop 15.4 $(\ex A \And \ex B \c x \in A \cup B \Iff x \in A \Or x \in B)$

\prop 15.5 $(\ex (A\cup B) \c x \in A \cup B \Iff x \in A \Or x \in B)$

\prop 15.6 $(\ex A \And \ex B \c x \in A \Or x \in B \Iff x \in A \cup B )$

\prop 15.7 $(\ex (A\cup B) \c x \in A \Or x \in B \Iff x \in A \cup B )$

\prop 15.8 $( x \in A \cup B \c x \in A \Or x \in B)$

\prop 15.9 $(\ex A \And \ex B \And (x \in A \Or x \in B) \c x \in A \cup B )$

\Prop 15.10 $(x \in A \cup B \And x \notin A \c x \in B)$

\Prop 15.11 $(x \in A \cup B \And x \notin B \c x \in A)$

\Prop 15.12 $(x \in A \And \ex B \c x \in A \cup B)$

\Prop 15.13 $(x \in B \And \ex A \c x \in A \cup B)$

\Prop 15.14 $(x \in A \And \ex (A \cup B) \c x \in A \cup B)$

\Prop 15.15 $(x \in B \And \ex (A \cup B) \c x \in A \cup B)$

\Prop 15.16 $(A \cup B \ident B\cup A)$

\Prop 15.17 $((A \cup B) \cup C \ident A \cup (B \cup C))$

\Prop 15.18 $(A \cup (B \cup C) \ident (A \cup B) \cup C)$

\Prop 15.19$(A \cup \e \ident A)$

\Prop 15.20$(\e \cup A  \ident A)$

\Prop 15.21 $(\ex (A \cup B) \c A \i A \cup B)$

\Prop 15.22 $(\ex (A \cup B) \c B \i A \cup B)$

\Prop 15.23 $(\ex A \And \ex B \c A \i A \cup B)$

\Prop 15.24 $(\ex A \And \ex B \c B \i A \cup B)$

\Prop 15.25 $(A\i B \Iff B = A\cup B )$

\Prop 15.26 $(A\i B \Iff B = B\cup A )$

\Prop 15.27 $(A\i B \Iff  B\cup A = B )$

\Prop 15.28 $(A\i B \Iff  A\cup B = B)$

\Prop 15.29 $(A \cup B \i C \Iff A \i C \And B \i C)$

\Prop 15.30 $(A \cup B \i C \c A \i C \And B \i C)$

\Prop 15.31 $(A \i C \And B \i C \c A \cup B\i C)$

\Prop 15.32 $(A \i C \And B \i D \c A \cup B \i C \cup D)$

\Prop 15.33 $(A \i C \And B \i C \c A \cup B\i C)$

\Prop 15.34 $(A \i C \And B \i C \Iff A \cup B\i C)$

\Prop 15.35 $(A \cup B \i C \c A \i C)$

\Prop 15.36 $(A \cup B \i C \c B \i C)$

\Prop 15.37 $(A \cup B = C \c A \i C)$

\Prop 15.38 $(A \cup B = C \c B \i C)$

\Prop 15.39 $(C = A \cup B \c A \i C)$

\Prop 15.40 $(C = A \cup B \c B \i C)$

\Prop 15.41 $(A\i B \And \ex C\c A\cup C \i B\cup C)$

\Prop 15.42 $(A\i B \And \ex C\c C \cup A \i C \cup  B)$

\Prop 15.43 $(A\i B \cup C \And A \cap B = \e \c A \i C)$

\Prop 15.44 $(\setof x \pbar x \cup \setof x \qbar x = \setof x (\pbar x\Or \qbar x))$

\Prop 15.45 $( \setof x (\pbar x\Or\qbar x) = \setof x \pbar x \cup \setof x \qbar x)$

\Prop 15.46 $(A \cup \e \ident A)$

\Prop 15.47 $(\e \cup A \ident A)$

\Prop 15.48 $(\ex A \c A\cup \e = A)$

\Prop 15.49 $(\ex A \Iff A \cup \Cmpl A = \U)$

\Prop 15.50 $(\ex A \c A \cup \Cmpl A = \U)$

\Prop 15.51 $(\ex A \Iff \Cmpl A \cup A = \U)$

\Prop 15.52 $(\ex A \c \Cmpl A \cup  A = \U)$

\Prop 15.53 $(\ex A \c \Cmpl A \cap  A = \e)$

\Prop 15.54 $(\ex B \c A \ident(A\cap B)\cup(A \cap \Cmpl B))$

\Prop 15.55 $(A \cup B \ident B \cup A)$

\Prop 15.56 $(A \cup A \ident A)$

\Prop 15.57 $(\Cmpl(A \cup B) \ident \Cmpl A \cap \Cmpl B)$

\Prop 15.58 $(\Cmpl(A \cap B) \ident \Cmpl A \cup \Cmpl B)$

\Prop 15.59 $((A \cap B) \cup C \ident (A \cup C)\cap(B\cup C))$

\Prop 15.60 $((A \cup C)\cap(B\cup C)\ident(A \cap B)\cup C)$

\Prop 15.61 $(C \cup (A \cap B)\ident (C\cup A)\cap(C\cup B))$

\Prop 15.62 $((C \cup A )\cap(C\cup B)\ident C\cup(A \cap B))$

\Prop 15.63 $((A \cup B) \cap C \ident (A \cap C)\cup(B\cap C))$

\Prop 15.64 $((A \cap C)\cup(B\cap C)\ident(A \cup B)\cap C)$

\Prop 15.65 $(C \cap (A \cup B)\ident (C\cap A)\cup(C\cap B))$

\Prop 15.66 $((C \cap A )\cup(C\cap B)\ident C\cap(A \cup B))$

\Prop 15.67 $(\ex A \And \ex B \c \Each x \in A \cup B \pbar x\Iff  \Each x \in A \pbar x
\And \Each x \in B \pbar x)$

\Prop 15.68 $(\ex A \And \ex B \c  \Each x \in A \pbar x \And \Each x \in B \pbar x\Iff  
\Each x \in A \cup B \pbar x)$

\lineb

\chap{16. Ternary Unions}

\noindent{Definition}

\prop 16.1 $(A\cup B \cup C \ident (A \cup B) \cup C)$

\noindent{Theorems}

\prop 16.2 $(A\cup B \cup C \ident A \cup (B \cup C))$

\prop 16.3 $((A\cup B) \cup C \ident A \cup B \cup C)$

\prop 16.4 $(A\cup (B \cup C) \ident A \cup B \cup C)$

\prop 16.5 $(A\cup  B \cup C  \ident A \cup C \cup B)$

\prop 16.6 $(A\cup  B \cup C  \ident B \cup A \cup C)$

\lineb

\chap{17. Set Difference}	

\noindent{Definition}

\prop 17.1 $((A \setdif B) \ident (A \cap \Cmpl B))$

\noindent{Theorems}

\prop 17.2 $(\ex(A\setdif B)\Iff \ex A \And \ex B)$

\prop 17.3 $(x \in A \setdif B \c x \notin B)$

\prop 17.4 $(x \in A \setdif B \c \Not(x \in B))$

\prop 17.5 $(x\in A\setdif B \Iff x \in A\And x\notin B)$

\prop 17.6 $(x\in A\setdif B \Iff x \in A\And \Not(x\in B))$

\prop 17.7 $(x\in A\setdif B \Iff x \in A\And x\in \Cmpl B)$

\prop 17.8 $(A \setdif B \ident A \cap \Cmpl B)$

\prop 17.9 $(x \in A\setdif B \c x \in \Cmpl B)$

\Prop 17.10 $(x \in A\setdif B \c x \in A)$

\Prop 17.11 $(x \in A \And x \notin B \c x \in A\setdif B)$

\Prop 17.12 $(x \in A \And \ex B \And \Not (x\in B)\c x \in A \setdif B)$

\Prop 17.13 $(A \setdif B \in \U \Iff A \in \U \And \ex B)$

\Prop 17.14 $(A \i B \cup C \c A \setdif C \i B)$

\Prop 17.15 $(A \i B \cup C \c A \setdif B \i C)$

\Prop 17.16 $(C= A \setdif B \c C \i A)$

\Prop 17.17 $(C = A \setdif B \c C \i \Cmpl  B)$

\Prop 17.18 $(\ex A \And \ex B \c A \setdif B  \i A)$

\Prop 17.19 $(\ex A \And \ex B \c A \setdif B  \i \Cmpl B)$

\Prop 17.20 $(A \setdif (A \setdif B) \ident A \cap B)$

\Prop 17.21 $(A \setdif (A \cap B) \ident A \setdif B)$

\Prop 17.22 $((A \setdif B) \setdif B \ident A \setdif B)$

\Prop 17.23 $((A \cup B)\setdif C \ident (A \setdif C) \cup (B\setdif C))$

\Prop 17.24 $(A \setdif B = \e \Iff A \i B)$

\Prop 17.25 $(\e = A \setdif B\Iff A \i B)$

\Prop 17.26 $(A \setdif B  = A \Iff A \cap B = \e)$

\Prop 17.27 $(A = A \setdif B \Iff A \cap B = \e)$

\Prop 17.28 $(\ex A \And \ex B \c A \setdif B \i A)$

\Prop 17.29 $(\ex B \c A \ident (A \setdif B)\cup (A \cap B))$

\Prop 17.30 $(\ex A \And B \i C \c A \setdif C \i A \setdif B)$

\Prop 17.31 $(\ex A \c A \setdif A = \e)$

\lineb

\chap{18. Symmetric Difference}	

\noindent{Definition}

\prop 18.1 $((a \symdif b)\ident((a \cup b) \setdif (a \cap b)))$

\noindent{Theorems}

\prop 18.2 $((a \symdif b)\ident((a \setdif b) \cup (b \setdif a)))$

\prop 18.3 $(\ex(a\symdif b) \Iff \ex a \And \ex b)$

\prop 18.4 $( x \in a\symdif b \Iff x \in  a \Onr x \in b)$

\prop 18.5 $(\ex a  \c  a \symdif a = \e)$

\prop 18.6 $(a \symdif \e \ident a)$

\prop 18.7 $(\e \symdif a \ident a)$

\prop 18.8 $( a \symdif b = \e \Iff a = b)$

\prop 18.9 $(a \symdif (b \symdif c) \ident (a \symdif b) \symdif c)$

\Prop 18.10 $(a \cap (b \symdif c) \ident (a \cap b) \symdif (a \cap c))$

\Prop 18.11 $((A \symdif B)\ident ((A \cup B) \setdif (A \cap B)))$

\Prop 18.12 $(\ex (A\symdif B) \Iff \ex A \And \ex B)$

\Prop 18.13 $(\ex A \c A \symdif A = \e)$

\Prop 18.14 $(A \symdif \e \ident A)$

\Prop 18.15 $(\e \symdif A \ident A)$

\Prop 18.16 $(A \symdif B = \e \Iff A = B)$

\Prop 18.17 $(\e = A \symdif B \Iff A = B)$

\Prop 18.18 $(x \in A\symdif B\Iff (x \in A \And \Not(x \in B))
\Or ( x \in B \And \Not(x \in A)))$

\Prop 18.19 $(x \in A\symdif B\Iff (x \in A \And x \notin B)
\Or ( x \in B \And x \notin A))$

\Prop 18.20 $(A \symdif B \ident B \symdif A)$

\Prop 18.21 $((A \symdif B )\symdif C \ident A \symdif (B\symdif C)) $

\Prop 18.22 $(A \symdif (B \symdif C )\ident (A \symdif B)\symdif C) $

\Prop 18.23 $(A \cap B = \e \Iff A \cup B = A \symdif B)$

\Prop 18.24 $(A \setdif B = A \symdif B \Iff B \i A)$

\Prop 18.25 $((A \symdif B) \cap C \ident (A \cap C)\symdif (B\cap C))$

\Prop 18.26 $(C \cap (A \symdif B) \ident (C \cap A )\symdif (C \cap B))$

\Prop 18.27 $(\ex C \And A = B \c C \symdif A = C \symdif B)$

\Prop 18.28 $((A \symdif B) \setdif C \ident (A \setdif C)\symdif (B\setdif C))$

\Prop 18.29 $( (A \setdif C)\symdif (B\setdif C) \ident (A \symdif B) \setdif C )$



\Prop 18.30 $(A \cap B = \e \c \One x \in A \cup B\pbar x
\Iff (\One x \in A \pbar x \And \Not\Some x \in B \pbar x) \Or
( \Not\Some x \in A \pbar x\And \One x \in B \pbar x  ))$
\lineb

\chap{19. Singletons, Doubletons, Etc.}

\noindent{Definitions}

\prop 19.1 $(\{a,b\} \ident (a,b, \in \U \cond \setof t(t = a \Or t = b)))$

\prop 19.2 $(\{a,b,c\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c)))$

\prop 19.211 $(\{a,b,c,d\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t = d )))$

\prop 19.212 $(\{a,b,c,d,e\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t = d \Or t =e)))$

\prop 19.213 $(\{a,b,c,d,e,f\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t = d \Or t =e \Or t =f)))$

\prop 19.214 $(\{a,b,c,d,e,f,g\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g)))$

\prop 19.215 $(\{a,b,c,d,e,f,g,h\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h)))$

\prop 19.216 $(\{a,b,c,d,e,f,g,h,i\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h \Or t=i)))$

\prop 19.217 $(\{a,b,c,d,e,f,g,h,i,j\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h \Or t=i \Or t=j)))$

\prop 19.218 $(\{a,b,c,d,e,f,g,h,i,j,k\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h \Or t=i \Or t=j \Or t=k)))$

\prop 19.219 $(\{a,b,c,d,e,f,g,h,i,j,k,l\} \ident (a,b,c, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h \Or t=i \Or t=j \Or t=k \Or t=l)))$

\prop 19.220 $(\{a,b,c,d,e,f,g,h,i,j,k,l,m\} \ident (a,b,c,d,e,f,g,h,i,j,k,l,m, \in \U \cond \setof t(t = a \Or t = b \Or t = c \Or t=d \Or t=e \Or t =f \Or t=g \Or t=h \Or t=i \Or t=j \Or t=k \Or t=l \Or t=m)))$

\noindent{Theorems}

\prop 19.3 $(x \in\{x\} \Iff x \in \U)$

\prop 19.4 $(y \in \{x\} \Iff y = x \And x \in \U)$

\prop 19.5 $(x \in \U \c y \in \{x\}\Iff y = x)$

\prop 19.6 $(\ex \{x\} \Iff x \in \U)$

\prop 19.7 $(\ex \{x\} \Iff \{x\} \in \U)$

\prop 19.8 $(\ex\{x\} \c \ex x)$

\prop 19.9 $(A = \{x\} \c x \in A)$

\Prop 19.10 $(\ex \{x\}\Iff x\in\{x\})$

\Prop 19.11 $(\ex \{x\} \Iff \e\ne\{x\})$

\Prop 19.12 $(\ex \{x,y\} \Iff \e\ne\{x,y\})$

\Prop 19.13 $(\{x\}\in \U \Iff x \in \U)$

\Prop 19.14 $(\ex\{x\} \c y \in \{x\} \Iff y = x)$

\Prop 19.15 $(x \in \U \c y \notin \{x\} \Iff y \ne x)$

\Prop 19.17 $(x \in \U \c y = x \Iff y \in \{x\} )$

\Prop 19.18 $(y \in \{x\} \c y = x)$

\Prop 19.19 $(z \in \{x,y\} \c z = x \Or z = y)$

\Prop 19.20 $(x,y,\in \U \c z \in \{x,y\} \Iff z = x \Or z = y)$

\Prop 19.21 $(A = \{x,y\} \c x \in A)$

\Prop 19.22 $(A = \{x,y\} \c y \in A)$

\Prop 19.23 $(A = \{x,y\} \c x \in A \And y \in A)$

\Prop 19.24$(A = \{x,y\} \c  z \in A \Iff z = x \Or z = y)$

\Prop 19.25 $(\{x,y\} \ident \{y,x\})$

\Prop 19.26 $(\{x,y\} \ident \{x\}\cup \{y\})$

\Prop 19.27 $(x,y,\in A\Iff \{x,y\}\i A)$

\Prop 19.28 $(x,y,\in A\c \{x,y\}\i A)$

\Prop 19.29 $(z = \{x,y\} \And x,y,\in A\c z \i A)$

\Prop 19.30 $(x \in A \Iff \{x\} \i A)$

\Prop 19.31 $(\{x\}\i A \Iff \e\ne\{x\}\i A)$

\Prop 19.32 $(\{x,y\}\i A\Iff \e\ne\{x,y\}\i A)$

\Prop 19.33 $(\{x\} \i C \And \{y\} \i C \c \{x,y\}\i C)$

\Prop 19.34 $(\{x\} \i C \And \{y\} \i C \Iff \{x,y\}\i C)$

\Prop 19.35 $(x \in A \c \{x\} \i A)$

\Prop 19.36 $(\{x\} \i A \c x \in A)$

\Prop 19.37 $(x \in \U \c \{x\} \in \U)$

\Prop 19.38 $(x \in \U \Iff \{x\} \in \U)$

\Prop 19.39 $(\{x\}\in \U \c x \in \U)$

\Prop 19.40 $(x,y, \in A \c \{x,y\} \i A)$

\Prop 19.41 $(\{x,y\} \i A \c x,y, \in A)$

\Prop 19.42 $(x,y, \in \U \c \{x,y\} \in \U)$

\Prop 19.43 $(x,y, \in \U \Iff \{x,y\} \in \U)$

\Prop 19.44 $(\{x,y\}\in \U \c x,y, \in \U)$

\Prop 19.45 $(\ex\{x,y\} \Iff x \in \U \And y \in \U)$

\Prop 19.46 $(\e \ne A \i \{x\} \Iff A = \{x\})$

\Prop 19.47 $(\ex x \Iff x \in \U\c y \in\{x\}\Iff y=x)$

\Prop 19.48 $(\ex x \Iff x \in \U\c y \notin\{x\}\Iff y\ne x)$

\lineb

\chap{20. Indexed Intersections}	

\noindent{Definitions}

\prop 20.1 $(\bigcap x; \pbar x \ubar x \ident (\Each x;\pbar x \ex \ubar x
\cond \setof y \Each x;\pbar x (y \in \ubar x)))$

\prop 20.2 $(\bigcap x,y; \pbarp xy \ubarp xy \ident (\Each x,y;\pbarp xy \ex \ubarp xy
\cond \setof z \Each x,y;\pbarp xy (z \in \ubarp xy)))$

\noindent{Theorems}

\prop 20.3 $(\ex \bigcap x; \pbar x \ubar x \Iff
	\Each x; \pbar x \ex \ubar x)$

\prop 20.4$(\Some x;\pbar x (\ubar x \i y) \And \ex \bigcap x ;\pbar x \ubar x
	\c \bigcap x;\pbar x \ubar x \i y)$

\prop 20.5$(\Each x;\pbar x (y \i \ubar x) \And \ex y
	\c y \i \bigcap x;\pbar x \ubar x )$

\prop 20.6 $(\ex y \c \Each x;\pbar x(y \i \ubar x)
	\Iff y \i \bigcap x;\pbar x \ubar x)$

\prop 20.7 $(\Some x \pbar x \c \Each x;\pbar x(y \i \ubar x)
	\Iff y \i \bigcap x;\pbar x \ubar x)$

\prop 20.8 $(\Each x (\pbar x \c \vbar x = \wbar x )\c 
	\bigcap x ; \pbar x \vbar x = \bigcap x; \pbar x \wbar x)$

\prop 20.9 $(\Each x (\pbar x \c \wbar x = \vbar x )\c 
	\bigcap x ; \pbar x \vbar x = \bigcap x; \pbar x \wbar x)$

\Prop 20.10 $(\ex A \And x \in \U \c x \in 
	\bigcap y \in A\ubar y \Iff \Each y \in A (x \in \ubar y))$

\Prop 20.11 $(x \in \bigcap y;\pbar y \ubar y \Iff 
	\Each y;\pbar y (x \in \ubar y) \And x \in \U)$

\Prop 20.12 $(x \in \bigcap y;\pbar y \ubar y \c \Each y;\pbar y(x \in \ubar y))$


\Prop 20.13 $(x \in \U \c 
	\Each y;\pbar y (x \in \ubar y) \Iff x \in \bigcap y;\pbar y \ubar y )$

\Prop 20.14 $(\Some y \pbar y \c 
	\Each y;\pbar y (x \in \ubar y) \Iff x \in \bigcap y;\pbar y \ubar y )$

\Prop 20.15 $(A \ne \e \c 
	\Each y \in A (x \in \ubar y) \Iff x \in \bigcap y \in A \ubar y )$

\Prop 20.16 $(x \in \ubar y \And \pbar y \And \ex y \And 
	\Each z;\pbar z \ex\ubar z \c x \in \bigcap z;\pbar z \ubar z)$

\Prop 20.17 $(x \in \ubar y \And y \in A \And \Each z \in A \ex\ubar z
	\c x \in \bigcap z\in A \ubar z)$


\Prop 20.18 $(x \in \bigcap y;\pbar y \ubar y \Iff
	\Each y;\pbar y(x \in \ubar y) \And x \in \U)$ 

\Prop 20.19 $(x \in \bigcap y;\pbar y \ubar y \And \pbar y \And \ex y 
	\c x \in \ubar y)$

\Prop 20.20 $(x \in \bigcap y \in A \ubar y \And y \in A \c x \in \ubar y)$

\Prop 20.21 $(\Some y \pbar y 
	\c x \in \bigcap y;\pbar y \ubar y \Iff \Each y;\pbar y (x \in \ubar y))$

\Prop 20.22 $(\Some x \pbar x 
	\c \bigcap x;\pbar x \setof y \pbarp xy = \setof y \Each x;\pbar x \pbarp xy)$

\Prop 20.23 $(\Some x \pbar x 
	\c \setof y \Each x;\pbar x \pbarp xy = \bigcap x;\pbar x \setof y \pbarp xy)$

\Prop 20.24 $(\Not \Some x \pbar x \c \bigcap x;\pbar x \ubar x = \U)$

\Prop 20.25 $(\bigcap x \in \e \ubar x = \U)$

\Prop 20.26 $(\Each x(\pbar x \Iff \qbar x) \c 
	\bigcap x;\pbar x \ubar x \ident \bigcap x;\qbar x \ubar x)$


\Prop 20.27 $(\bigcap x;(\pbar x \And \qbar x) \ubar x 
	\ident \bigcap x;\pbar x \ubar x \cap \bigcap x;\qbar x \ubar x)$

\Prop 20.28 $(A = B \cap C \c
\bigcap x \in A \ubar x \ident \bigcap x \in B \ubar x\cap\bigcap x \in C \ubar x)$

\Prop 20.29 $(\Each x(\pbar x \c \qbar x)  \And \Each x;\qbar x \ex \ubar x 
	\c \bigcap x;\qbar x \ubar x \i \bigcap x;\pbar x \ubar x)$

\Prop 20.30 $(\Each x(\pbar x \c \qbar x)  \And \ex \bigcap x;\qbar x \ubar x 
	\c \bigcap x;\qbar x \ubar x \i \bigcap x;\pbar x \ubar x)$


\Prop 20.31 $(A \i B  \And \Each x \in B \ex \ubar x 
	\c \bigcap x \in B \ubar x \i \bigcap x \in A \ubar x)$

\Prop 20.32 $(A \i B  \And \ex \bigcap x \in B \ubar x 
	\c \bigcap x \in B \ubar x \i \bigcap x \in A \ubar x)$

\Prop 20.33 $(\ex y \c \bigcap x = y \ubar x \ident \ubar y)$

\Prop 20.34 $(y \in \U \c \bigcap x \in \{y\} \ubar x \ident \ubar y)$

\Prop 20.35 $(\Each x (\pbar x \c \ubar x \ident \vbar x)
	\c \bigcap x ; \pbar x \ubar x \ident \bigcap x;\pbar x \vbar x)$

\Prop 20.36 $(\ex y \c \bigcap x;\pbar x(\ubar x \cup y)
	\ident \bigcap x;\pbar x\ubar x \cup y)$

\Prop 20.37 $(\ex y \c \bigcap x;\pbar x\ubar x \cup y
	\ident \bigcap x;\pbar x(\ubar x \cup y))$

\Prop 20.38 $(\ex y \c \bigcap x;\pbar x(y \cup \ubar x)
	\ident y \cup \bigcap x;\pbar x \ubar x)$

\Prop 20.39 $(\ex y \c y \cup \bigcap x;\pbar x\ubar x 
	\ident \bigcap x;\pbar x(y \cup \ubar x))$


\Prop 20.40 $(\Some x \pbar x \c \bigcap x;\pbar x(\ubar x \cup y)
	\ident \bigcap x;\pbar x\ubar x\cup y)$

\Prop 20.41 $(\Some x \pbar x \c \bigcap x;\pbar x\ubar x \cup y
	\ident \bigcap x;\pbar x(\ubar x\cup y))$

\Prop 20.42 $(\Some x \pbar x \c \bigcap x;\pbar x(y \cup \ubar x)
	\ident y \cup \bigcap x;\pbar x\ubar x)$

\Prop 20.43 $(\Some x \pbar x \c y \cup \bigcap x;\pbar x\ubar x 
	\ident \bigcap x;\pbar x(y \cup \ubar x))$

\Prop 20.44 $(\Each x;\pbar x \ex \ubar x \And \pbar y \And \ex y 
	\c \bigcap x;\pbar x \ubar x \i \ubar y)$

\Prop 20.45 $(\ex \bigcap x;\pbar x \ubar x \And \pbar y \And \ex y
	\c \bigcap x;\pbar x \ubar x \i \ubar y)$

\Prop 20.46 $(\Each x \in A \ex \ubar x \And y \in A
	\c \bigcap x \in A \ubar x \i \ubar y)$

\Prop 20.47 $(\Each x;\pbar x (B \i \ubar x) \And \ex B
	\c B \i \bigcap x;\pbar x \ubar x)$

\Prop 20.48 $(\Each x \in A (B \i \ubar x) \And \ex B
	\c B \i \bigcap x \in A \ubar x)$

\Prop 20.49 $(\Each x;\pbar x (B \i \ubar x) \And \Some x \pbar x
	\c B \i \bigcap x;\pbar x \ubar x)$

\Prop 20.50 $(\Each x \in A (B \i \ubar x) \And A \ne \e 
	\c B \i \bigcap x \in A \ubar x)$
\lineb


\chap{21. Indexed Unions}	

\noindent{Definitions}

\prop 21.1 $(\bigcup x ;\pbar x \ubar x \ident (\Each x;\pbar x \ex \ubar x
\cond \setof y \Some x;\pbar x (y \in \ubar x)))$

%\prop 21.2 $(\bigcup x,y; \pbarp xy \ubarp xy \ident (\Each x,y;\pbarp xy \ex \ubarp xy
%\cond \setof z \Some x,y;\pbarp xy (z \in \ubarp xy)))$

\noindent{Theorems}

\prop 21.3 $(\ex \bigcup x; \pbar x \ubar x \Iff
\Each x; \pbar x \ex \ubar x)$

\prop 21.4 $(\ex \bigcup x,y; \pbarp xy \ubarp xy \Iff
\Each x,y; \pbarp xy \ex \ubarp xy)$

\prop 21.5 $(z \ident \bigcup x; \pbar x \ubar x \c
\ex z \Iff \Each x ; \pbar x \ex \ubar x)$

\prop 21.6 $(z \ident \bigcup x; \pbar x \ubar x \And \Each x ; \pbar x \ex \ubar x\c
y \in z \Iff \Some x; \pbar x (y \in \ubar x))$

\prop 21.7 $(z \ident \bigcup x,y; \pbarp xy \ubarp xy \c
\ex z \Iff \Each x,y ; \pbarp xy \ex \ubarp xy)$

\prop 21.8 $(z \ident \bigcup x,y; \pbarp xy \ubarp xy \And \Each x,y;\pbarp xy \ex \ubarp xy \c
t \in z \Iff \Some x,y; \pbarp xy (t \in \ubarp xy))$

\prop 21.9$(\ex y \And \Each x;\pbar x (\ubar x \i y)
\c \bigcup x;\pbar x \ubar x \i y)$

\Prop 21.10$(\Some x\pbar x \And \Each x;\pbar x (\ubar x \i y)
	\c \bigcup x;\pbar x \ubar x \i y)$

\Prop 21.11$(A \ne \e \And \Each x \in A (\ubar x \i y)
	\c \bigcup x \in A \ubar x \i y)$

\Prop 21.12 $(\Each x;\pbar x(\ubar x \i y) \And \ex y
	\Iff \bigcup x;\pbar x \ubar x \i y )$

\Prop 21.13 $(\ex y \c \Each x;\pbar x(\ubar x \i y)
	\Iff \bigcup x;\pbar x \ubar x \i y)$

\Prop 21.14 $(\Some x \pbar x \c \Each x;\pbar x(\ubar x \i y)
	\Iff \bigcup x;\pbar x \ubar x \i y)$

\Prop 21.15$(A \ne \e \c \Each x \in A (\ubar x \i y)
	\Iff \bigcup x \in A \ubar x \i y)$


\Prop 21.16 $(\Each y\in A\ex\ubar y \c x \in 
\bigcup y \in A\ubar y \Iff \Some y \in A (x \in \ubar y))$

\Prop 21.17 $(x \in \bigcup y \in A\ubar y \Iff 
	\Some y \in A (x \in \ubar y) \And \Each y\in A\ex\ubar y)$

\Prop 21.18 $(\Each y\in A\ex\ubar y \c  
\Some y \in A (x \in \ubar y) \Iff 
x \in \bigcup y \in A\ubar y )$

\Prop 21.19 $(\Each y,z \in A\ex\ubarp yz \c  
\Some y,z \in A (x \in \ubarp yz) \Iff 
x \in \bigcup y,z \in A\ubarp yz )$

\Prop 21.20 $(x \in \bigcup y \in A \ubar y \c \Some y \in A(x \in \ubar y))$

\Prop 21.21 $(x \in \ubar y \And y \in A \And \Each z \in A \ex\ubar z
\c x \in \bigcup z\in A \ubar z)$


\Prop 21.22 $(x \in \bigcup y \in A \ubar y \Iff
\Some y \in A(x \in \ubar y) \And \Each y \in A \ex\ubar y)$ 

\Prop 21.23 $(\ex \bigcup y \in A \ubar  y \And y \in A \And x \in \ubar y \c
x \in \bigcup y \in A \ubar y )$

\Prop 21.24 $(\ex \bigcup y \in A \ubar  y \c
x \in \bigcup y \in A \ubar y \Iff \Some y \in A (x \in \ubar y))$

\Prop 21.25 $(x \in \bigcup y \in A \ubar  y \c
\Some y \in A (x \in \ubar y))$

\Prop 21.26 $(\ex A \c \bigcup x \in A \setof y \pbarp xy
=\setof y \Some x \in A \pbarp xy)$

\Prop 21.27 $(\ex A \c 
\setof y \Some x \in A \pbarp xy =
\bigcup x \in A \setof y \pbarp xy)$

\Prop 21.28 $(\bigcup x \in \e \ubar x = \e)$

\Prop 21.29 $(A = B \cup C \c
\bigcup x \in A \ubar x \ident \bigcup x \in B\ubar x\cup\bigcup x \in C\ubar x)$

\Prop 21.30 $(A \i B  \And \Each x \in B \ex \ubar x \c
\bigcup x \in A \ubar x \i \bigcup x \in B\ubar x)$

\Prop 21.31 $(A \i B  \And \ex\bigcup x \in B \ubar x \c
\bigcup x \in A \ubar x \i \bigcup x \in B\ubar x)$

\Prop 21.32 $(y \in \U \c
\bigcup x \in \{y\} \ubar x \ident \ubar y)$

\Prop 21.33 $(\Each x (\pbar x \c \ubar x \ident \vbar x)
\c \bigcup x ; \pbar x \ubar x \ident \bigcup x;\pbar x\vbar x)$

\Prop 21.34 $(\Some x  \pbar x \c \bigcup x;\pbar x
(\ubar x \cap y)\ident\bigcup x;\pbar x\ubar x\cap y)$

\Prop 21.35 $(\Some x  \pbar x \c \bigcup x;\pbar x
(y\cap\ubar x)\ident y\cap\bigcup x;\pbar x\ubar x)$

\Prop 21.36 $(\Some x  \pbar x \c 
\bigcup x;\pbar x\ubar x\cap y
\ident \bigcup x;\pbar x (\ubar x \cap y) )$

\Prop 21.37 $(\Some x  \pbar x \c 
y\cap\bigcup x;\pbar x\ubar x \ident \bigcup x;\pbar x
(y\cap\ubar x) )$

\Prop 21.38 $(\ex y \c \bigcup x;\pbar x
(\ubar x \cap y)\ident\bigcup x;\pbar x\ubar x\cap y)$

\Prop 21.39 $(\ex y \c \bigcup x;\pbar x
(y\cap\ubar x)\ident y\cap\bigcup x;\pbar x\ubar x)$

\Prop 21.40 $(\ex y \c
\bigcup x;\pbar x\ubar x\cap y
\ident \bigcup x;\pbar x (\ubar x \cap y) )$

\Prop 21.41 $(\ex y \c
y\cap\bigcup x;\pbar x\ubar x \ident \bigcup x;\pbar x
(y\cap\ubar x) )$

\Prop 21.42 $(\Each x;\pbar x \ex\ubar x \And \pbar y \And
\ex y \c \ubar y \i \bigcup x;\pbar x \ubar x)$

\Prop 21.43 $(\Each x \in A \ex\ubar x \And y \in A
\c \ubar y \i \bigcup x \in A \ubar x)$

\Prop 21.44 $(\Each x \in A (\ubar x \i B) \And \ex B
\c \bigcup x \in A \ubar x \i B)$

\Prop 21.45 $(\Each x ;\pbar x (\ubar x \i \vbar x )\c \bigcup x ; \pbar x \ubar x \i \bigcup x; \pbar x \vbar x)$


\Prop 21.46 $(\Each x (\pbar x \c \vbar x = \wbar x )\c \bigcup x ; \pbar x \vbar x = \bigcup x; \pbar x \wbar x)$

\Prop 21.47 $(\Each x (\pbar x \c \wbar x = \vbar x )\c \bigcup x ; \pbar x \vbar x = \bigcup x; \pbar x \wbar x)$

\Prop 21.48 $(\ex A \c A \ident \bigcup p \in A \{p\})$

\Prop 21.49 $(\ex A \c A = \bigcup p \in A \{p\})$
\lineb

\chap{22. Unary Intersection Operator}	

\noindent{Definition}

\prop 22.1 $(\PI B \ident (\ex B \cond \bigcap b \in B b))$

\noindent{Theorems}

\prop 22.2 $(\ex \PI A \Iff \ex A )$

\prop 22.3 $(a \in A \c \PI A \i a)$

\prop 22.4 $(\PI \e = \U)$

\prop 22.5 $(\PI\{x\} = x \Iff x \in \U)$

\prop 22.6 $(\PI A \in \U \Iff A \ne \e)$

\prop 22.7 $(A \ne \e \c x \in \PI A \Iff \Each a \in A(x \in a))$ 

\prop 22.8 $(A \i B \c \PI B \i \PI A)$

\prop 22.9 $(C = A \cup B \c \PI C = \PI A \cap \PI B)$

\Prop 22.10 $(B \ne \e \And \Each b \in B(a \i b) \c a \i \PI B)$

\Prop 22.11 $(\PI\bigcup x ;\pbar x \vbar x \ident \bigcup x ;\pbar x \PI\vbar x)$

\Prop 22.12 $(\Each x;\pbar x\ex\vbar x \c 
	\PI\bigcup x ;\pbar x \vbar x = \bigcup x ;\pbar x \PI\vbar x)$
\lineb

\chap{23. Unary Union Operator}	

\noindent{Definition}

\prop 23.1 $(\SI B \ident (\ex B \cond \bigcup b \in B b))$

\noindent{Theorems}

\prop 23.2 $(\ex A \Iff \ex \SI A)$

\prop 23.3 $(A = B \c \SI A = \SI B)$

\prop 23.4 $(\SI \e = \e)$

\prop 23.5 $( A = \SI\{x\} \c A = x)$

\Prop 19.16 $(x \in \U \Iff \SI\{x\} =  x)$

\prop 23.6 $(\ex A \And \ex B \c \SI B \i A \Iff \Each x \in B ( x \i A))$

\prop 23.7 $(\SI B \i A \Iff \ex A \And \ex B \And \Each x \in B ( x \i A))$

\prop 23.8 $(A = \SI B \And x \in B \c x \i A)$

\prop 23.9 $(x \i y \And y \in B \c x \i \SI B)$

\Prop 23.10 $(\Some y \in B(x \i y)\c x \i \SI B)$

\Prop 23.11 $(A = \SI B \Iff \ex A \And \ex B \And \Each x \in B(x \i A) \And \Each x \in A\Some y \in B(x \in y))$

\Prop 23.12 $(x \in \SI A \c \Some y \in A(x \in y))$

\Prop 23.13 $(x \in \SI A \Iff \Some y \in A (x \in y ))$

\Prop 23.14 $(x \in A \c x \i \SI A)$

\Prop 23.15 $(y \in x \And x \in A \c y \in \SI A)$

\Prop 23.16 $(A \i B \c \SI A \i \SI B)$

\Prop 23.17 $(\SI(A\cup B) \ident \SI A \cup \SI B)$

\Prop 23.18 $(\ex A \c \SI A = \bigcup x \in A x)$

\Prop 23.19 $(A \in \U \Iff \SI A \in \U)$

\Prop 23.20 $(\SI\bigcup x ;\pbar x \vbar x \ident \bigcup x ;\pbar x \SI\vbar x)$

\Prop 23.21 $(\Each x;\pbar x\ex\vbar x \c \SI\bigcup x ;\pbar x \vbar x = \bigcup x ;\pbar x \SI\vbar x)$
\lineb

\chap{24. The Power Set}	

\noindent{Recall definition}

\noindent{} 7.5 $(\sb x \ident (\ex x \cond \setof y (y \i x)))$

\noindent{Theorems}

\prop 24.1 $(\ex \sb A \Iff \ex A)$

\prop 24.2 $(x \in \sb A \Iff x \i A \And x \in \U)$

\prop 24.3 $(x \in \sb A \c x \i A )$

\prop 24.4 $(\sb A \in \U \Iff A \in \U)$

\prop 24.5 $(\sb A \ident (\ex A \cond \setof B(B\i A)))$

\prop 24.6 $(A\in \U \And B\in \U\c\sb(A \cap B) =  \sb A \cap \sb B)$

\prop 24.7 $(A \i B \c \sb A \i \sb B)$

\prop 24.8 $(\sb \e = \{\e\})$

\prop 24.9 $(x \in y \Iff \{x\} \in \sb y)$
\lineb

\chap{25. The Super Power Set}	

\noindent{Definition}

\prop 25.1 $(\sp x \ident (\ex x \cond \setof y (x \i y)))$

\noindent{Theorems}

\prop 25.2 $(\ex \sp A \Iff \ex A)$

\prop 25.3 $(x \in \sp A \Iff A \i x \And x \in \U)$

\prop 25.4 $(x \in \sp A \c A  \i x)$
\lineb

\chap{26. The Set of Singletons}	

\noindent{Definition}

\prop 26.1 $(\ss A \ident(\ex A \cond\setof \{x\}\ls x\in A\rs))$
 
\noindent{Theorems}

\prop 26.2 $(x \in \ss y \Iff \Some z \in y (x = \{z\}))$

\prop 26.3 $(\ex \ss y \Iff \ex y)$

\prop 26.4 $(y \in \ss x \And  z \ident \The z (z\in y) \c y = \{z\})$

\prop 26.5 $(y \in \ss x \And  z \ident \The z (z\in y) \c z\in x)$

\prop 26.6 $(y \in \ss x \And z \in y \c z \in x)$

\prop 26.7 $(x \in A \Iff \{x\} \in \ss A)$

\prop 26.8 $(\ex A \c \ss A \i \sb A)$


\prop 26.9 $(x \in a \Iff \{x\} \in \ss a)$



\lineb

\chap{27. Partitions}

\noindent{Definitions}

\prop 27.1 $(\disjoint \ident \setof A \Each x,y, \in A
(x \cap y \ne \e \c x = y))$

\prop 27.2 $((x \djn y) \Iff (x \cap y = \e))$

\prop 27.3 $(\partition A \ident \setof B \in \disjoint (\e \notin B \And  A = \SI B))$


\noindent{Theorems}

\prop 27.4 $(A \in \disjoint \Iff A \in \U \And  \Each x,y, \in A
(x \cap y \ne \e \c x = y))$

\prop 27.5 $(A \in \disjoint \And a\in A \And b \in A
\And a \cap b \ne \e \c a = b)$

\prop 27.6 $(A,B, \i C \in \disjoint
	\c \SI (A \cap B) = \SI A \cap \SI B)$

\prop 27.7 $(C \in \disjoint \And \Each x;\pbar x(\ubar x \i C) \And  
	\Some x \pbar x $
 $ \c \bigcap x;\pbar x \SI \ubar x
		=\SI \bigcap x;\pbar x \ubar x)$

\prop 27.8 $(A,B, \i C \in \disjoint
	\c \SI (A \setdif B) = \SI A \setdif \SI B)$

\prop 27.9 $(B \in \partition A \Iff B \in \disjoint \And \e \notin B \And A=\SI B)$
\lineb



\chap{28. General Induction}

\noindent{Definitions}
 
\prop 28.1 $(\Closure x \ubar x \ident (\Some x (\ubar x \i x)
	\cond \bigcap x;(\ubar x \i x) x))$

\prop 28.2 $(\confines x \ubar x \Iff 
\Each x\Each y(\ubar y \i y \And y \i x \c \ubar y \i y))$

\prop 28.3 $(\constricts x \ubar x \Iff 
\Each x\Each y(\ubar y \i y \And x \i y \c \ubar x \i \ubar y))$


\noindent{Theorems}

\prop 28.4 $(\ex \Closure x \ubar x
\Iff \Some x (\ubar x \i x))$

\prop 28.5 $(\ubar x \i x \c \Closure x \ubar x \i x)$

\prop 28.6 $(Q \ident \Closure x \ubar x \c \ex Q \Iff \Some x (\ubar x\i x ))$

\prop 28.7 $(Q \ident \Closure x \ubar x\And \Some x (\ubar x\i x ) \And \constricts x \ubar x
\c \ubar Q = Q)$

\prop 28.8 $(Q \ident  \Closure x \ubar x\And \ubar x \i x \c Q \i x)$

\prop 28.9 $(Q = \Closure x \ubar x \And \constricts x \ubar x \c \ubar Q = Q)$

\Prop 28.10 $(Q \ident (\pvar \cond \Closure x \ubar x)\And
(\pvar \c \Some x (\ubar x\i x )) \c \ex Q \Iff \pvar)$

\Prop 28.11 $(Q \ident (\pvar \cond \Closure x \ubar x)\And
(\pvar \c \Some x (\ubar x\i x ) \And \constricts x \ubar x) \c Q = \ubar Q \Iff \pvar)$

\Prop 28.12 $(Q \ident(\pvar\cond \Closure x\ubar x)\And \pvar \And \ubar x \i x \c Q \i x)$ 

\Prop 28.13 $(\constricts x \ubar x \And z = \Closure x \ubar x \c z = \ubar z)$


\Prop 28.14 $(\Each x\Each y (x \i y \c\ubar x\i\ubar y) 
	\And z = \Closure x \ubar x \c z = \ubar z)$

\Prop 28.15 $(\constricts x \ubar x \c 
	y = \Closure x \ubar x \Iff \ubar y \i y \And
	\Each x (\ubar x \i x \c y \i x))$
	\lineb


\chap{29. Finite Sets}

\noindent{Definition}

\prop 29.1 $(\fnt \ident \Closure A
(\{\e\}\cup \bigcup x \in A\bigcup y \in \U \{(x \cup \{y\})\}))$

\noindent{Theorems}


\prop 29.2 $\ex\fnt$

\prop 29.3 $(A\i  B \in \fnt \c A \in \fnt)$

\prop 29.4 $(A,B, \in \fnt \c A \cup B\in \fnt)$
\lineb

\chap{30. Ordinal Numbers}

The ordinal numbers are developed using 28.1.  
\lineb

\prop 30.1 $(\scsr x \ident (x \cup \{x\}))$

\Prop 30.2 $(\Omega \ident \Closure S \setof z \i S (\SI z \i z))$

\Prop 30.3 $(\omega \ident (\fnt \cap \Omega))$
\lineb


\chap{31. Ordered Pairs and Tuples}
	\lineb  

A tuple is indexed by an ordinal number.


\noindent{Definitions}

%precedence= 17
\prop 31.1 $((a \strcomma b) \ident \{\{a\},\{a,b\}\})$
 
\prop 31.2 $(\brct x y \ident (\ex x \And \ex y \cond\setof (a\strcomma b)\ls a \in x, b \in y\rs))$

\prop 31.3 $((a, b) \ident (\brct \{\e\} (\ss a \cup\{\e\})\cup \brct \{\scsr \e\}(\ss b\cup\{\e\})))$

\Prop 31.12 $(\bsvs Tx \ident (T \i \brct \U \U \And x \in \U \cond \setof y 
(x\strcomma y\in T)))$

\Prop 31.14 $(\bsdmn T \ident (T \i \brct \U\U \cond \setof x (\bsvs Tx \ne \e)))$

\Prop 31.15 $(\tuplep T \Iff (T \i \brct \U\U \And \Each i \in \bsdmn T
(\SI \bsvs Ti = \ss \bsvs Ti \cup \{\e\})))$

\Prop 31.16 $(\crd i T \ident (\tuplep T \And i \in \bsdmn T \cond \SI \bsvs Ti))$

\Prop 31.17 $(\crd\p T \ident \crd \e T)$

\Prop 31.18 $(\crd\pp T \ident \crd \scsr\e T)$

\Prop 31.19 $(\tup x; \pbar x \ubar x \ident \bigcup x; \pbar x 
	\brct \{x\} (\{\e\}\cup \ss \ubar x))$ 

\Prop 31.20 $(\Tup x; \pbar x \ubar x \ident 
\setof T (\tuplep T \And \bsdmn T = \setof x \pbar x \And 
	\Each x; \pbar x (\crd x T \in \ubar x)))$


\noindent{Theorems}


\prop 31.4 $((a,b) = (c,d) \Iff a = c \And b = d)$

\prop 31.5 $((a,b) \in \U \Iff a \in \U \And b\in\U)$

\prop 31.6 $(\ex(a,b)\Iff \ex a\And \ex b)$

\prop 31.7 $(\ex(a,b)\c \ex a)$

\prop 31.8 $(\ex(a,b)\c  \ex b)$

\prop 31.9 $((a,b)\in A \c \ex a \And \ex b)$

\Prop 31.10 $((a,b) \in \U \c a \in \U)$

\Prop 31.11 $((a,b) \in \U \c b \in \U)$
	\lineb  

\chap{32. Relations}

\noindent{Definitions}

\prop 32.1 $((A \lilx B) \ident (\ex A \And \ex B \cond \setof (x,y)\ls x \in A, y \in B\rs))$

\prop 32.2 $(\relationp R \Iff (R \i \U \lilx \U))$

\prop 32.3 $(\vs Ra \ident(\relationp R \And \ex a\cond\setof b((a,b)\in R)))$ 

\prop 32.4 $(\hs Rb \ident (\relationp R \And \ex b\cond\setof a((a,b)\in R)))$ 

\prop 32.5 $(\Dmn R \ident (\relationp R \cond \setof a \Some b((a,b)\in R)))$

\Prop 32.38 $(\strc RA \ident (\relationp R \cond R \cap (A \lilx \U)))$ 

\Prop 32.39 $(\relation \ident \setof R \relationp R)$

\prop 33.5 $(\inv f \ident \setof (y,x) \ls x,y ;((x,y)\in f)\rs)$

\noindent{Theorems}

\prop 32.6 $(A \in \U \And B \in \U \c A \lilx B \in \U)$

\prop 32.7 $(A \in \U \c A \lilx A \in \U)$

\prop 32.8 $(\relationp R \c \ex R)$

\prop 32.9 $(A \i B \And \relationp R \c \strc RA \i \strc RB)$

\Prop 32.11 $(\relationp R \c x \in \Dmn R \Iff \Some y((x,y) \in R))$

\Prop 32.12 $(\relationp R \And (x,y) \in R \c x \in \Dmn R)$

\Prop 32.13 $(\relationp R\Iff \ex R \And \Each p \in R \Some x,y (p = (x,y)))$

\Prop 32.14 $(\ex R \And \Each p \in R\Some x (p = (\ubar x,\vbar x)) \c \relationp R)$

\Prop 32.15 $(\ex R \And \Each p \in R\Some x,y (p = (\ubarp xy,\vbarp xy)) \c \relationp R)$

\Prop 32.16 $(\ex R \And \Each p \in R\Some x ;\pbar x(p = (\ubar x,\vbar x)) \c \relationp R)$

\Prop 32.17 $(\ex R \And\Each p \in R\Some x,y;\pbarp xy (p = (\ubarp xy,\vbarp xy)) \c \relationp R)$

\Prop 32.18 $(R \ident \setof (x,y) \ls x,y;\pbarp xy\rs \c \relationp R)$
 
\Prop 32.19 $(R \ident \setof (x,y) \ls x,y;\pbarp xy\rs \c \ex R)$
 
\Prop 32.20 $(R \ident \setof (x,y) \ls x,y;\pbarp xy\rs \c (u,v) \in R \Iff \pbarp uv \And u \in \U \And v \in \U)$

\Prop 32.21 $(R \ident \setof (x,y) \ls x,y;\pbarp xy\rs \And \Each x,y(\pbarp xy \c x \in \U \And y \in \U) \c (u,v) \in R \Iff \pbarp uv)$

\Prop 32.22 $(R \ident \setof (x,y) \ls x,y \in S ;\pbarp xy\rs \c (u,v) \in R \Iff (u,v) \in S \And \pbarp uv)$

\Prop 32.23 $(R \ident \setof (x,y) \ls x,y \in S ;\pbarp xy\rs \And \ex S\c R \i S)$ 

\Prop 32.24 $(R \ident \setof (x,y) \ls x,y,\in S ;\pbarp xy\rs \c (u,v) \in R \Iff u,v, \in S \And \pbarp uv)$

\Prop 32.25 $(\relationp R \c u \in \Dmn R \Iff \Some v ((u,v) \in R)) $

\Prop 32.26 $(u \in \Dmn R \c \Some v ((u,v) \in R)) $

\Prop 32.27 $(\relationp R \And (u,v) \in R \c u \in \Dmn R) $

\Prop 32.28 $(\strc RA \ident(\relationp R \cond \setof (x,y)\ls x,y\in R;(x \in A)\rs))$

\Prop 32.29 $(\ex \strc fA \Iff \relationp f \And \ex A)$

\Prop 32.30 $(A \i B \And \relationp R \c \strc R A \i \strc R B)$

\Prop 32.31 $(\ex (A \lilx B) \Iff \ex A \And \ex B)$ 

\Prop 32.32 $(R \i A \lilx B \c \Dmn R \i A)$

\Prop 32.33 $(\Dmn R \i A \c \Some B (R \i A \lilx B))$

\Prop 32.333 $(\rng R \ident (\relationp R \cond \setof y\Some x((x,y)\in R)))$

\Prop 32.334 $(y \in \rng R \c \Some x((x,y)\in R))$

\Prop 32.335 $(R \i S \And \relationp S \c \rng R \i \rng S)$

\Prop 32.337 $(R \i A \lilx B \c \rng R \i B)$

\Prop 32.34 $(R \i A \lilx B \c \relationp R)$

\Prop 32.35 $(R \i S \And \relationp S \c \Dmn R \i \Dmn S)$

\Prop 32.36 $(\relationp R \c R \i S \Iff \Each x,y((x,y) \in R \c (x,y) \in S)\And \ex S)$

\Prop 32.37 $(\relationp R \And \Each x,y((x,y) \in R \c (x,y) \in S) \And \ex S\c R \i S)$

\lineb

\chap{33. Functions}
\lineb

The function constructor is denoted with a reverse lambda notation, named
``lonzo'' by Morse in honor of Alonzo Church.
	\lineb

\noindent{Definitions}

\prop 33.1 $(\functionp f \Iff
(\relationp f \And \Each x \Unq y((x,y)\in f)))$

\prop 33.2 $(\function \ident \setof f \functionp f)$

\prop 32.511 $(\dmn f \ident (\functionp f \cond \Dmn f))$ 


\prop 33.3 $(\.fx \ident (\functionp f
\cond \The y ((x,y) \in f)))$

\prop 33.4 $(\lonzo x;\pbar x \ubar x \ident \setof (x,\ubar x)\ls x;\pbar x \rs )$

\prop 33.6 $(\onetoonep f \Iff (\functionp f \And \functionp \inv f))$

\prop 33.7 $(\onetoone \ident \setof f \onetoonep f)$

\prop 33.8 $(\.f : A \into B \Iff (\functionp f \And \dmn f = A \And \rng f \i B))$

\prop 33.9 $(\.f : A \onto B \Iff (\functionp f \And \dmn f = A \And \rng f = B))$

\Prop 33.10 $(\.f : A \oneto B \Iff
(\functionp f \And \dmn f = A \And \rng f \i B \And \functionp \inv f))$

\Prop 33.11 $(\.f : A \Iff B \Iff
(\functionp f \And \dmn f = A \And \rng f = B \And \functionp \inv f))$

\Prop 33.12 $(\histar f A \ident (\functionp f \And \ex A\cond\setof x (\.fx \in A)))$

\Prop 33.13 $(\lostar f A\ident(\functionp f \And \ex A\cond \setof \.fx \ls x \in A\rs))$

	\lineb

\noindent{Theorems}

\Prop 33.14 $(\functionp R \c \relationp R)$

\Prop 33.15 $(\functionp f \c \ex f)$

\Prop 33.16 $(\functionp f \c \rng f \i \U)$

\Prop 33.17 $(\functionp f \And (x,a) \in f \And (x,b) \in f \c a = b)$

\Prop 33.18 $(\ex \.fx \Iff x \in \dmn f)$

\Prop 33.19 $(\ex \.fx \c \.fx \in \U \And x \in \U)$

\Prop 33.20 $(\functionp f\c \Dmn f = \dmn f)$

\Prop 33.21 $(x \in \dmn f \c \.fx \in \rng f)$

\Prop 33.22 $(x \in \dmn f \c \ex \.fx)$

\Prop 33.23 $(f \in \function \And x \in \dmn f \c \ex \.fx)$

\Prop 33.24 $(f \in \function \And x \in \dmn f
	\c \.fx \in \rng f)$  

\Prop 33.25 $(x \in \dmn f \c \.fx \in \rng f)$

\Prop 33.26 $(x \in\dmn f \c \ex\.fx)$

\Prop 33.27 $(x \in\dmn f \Iff \ex\.fx)$

\Prop 33.28 $(\ex \dmn f \Iff \functionp f)$

\Prop 33.29 $(y \in \rng f \Iff \Some x (y = \.fx))$

\Prop 33.30 $(y = \.fx \c y \in \rng f)$

\Prop 33.31 $(y = \.fx \c x \in \dmn f)$

\Prop 33.32 $(\.fx  = y \c y \in \rng f)$

\Prop 33.33 $(\.fx  = y \c x \in \dmn f)$

\Prop 33.34 $(\ex A \And \ex \dmn f \And \Each n \in \dmn f(\.fn \in A)\c \rng f \i A)$

\Prop 33.35 $(\dmn f\ne\e \And \Each n \in \dmn f(\.fn \in A)\c \rng f \i A)$

\Prop 33.36 $(\ex A \And \ex \dmn f \c \Each n \in \dmn f(\.fn \in A)\Iff \rng f \i A)$

\Prop 33.37 $(\ex A \And \ex \dmn f \c \rng f \i A \Iff \Each n \in \dmn f(\.fn \in A))$

\Prop 33.38 $(\ex \.fx \c x \in \dmn f)$

\Prop 33.39 $(\ex \.fx \c \ex f)$

\Prop 33.40 $(\ex\.fx \c \.fx \in \rng f)$

\Prop 33.41 $(\ex\.fx \c x \in \U)$

\Prop 33.42 $(\ex\.fx \c \.fx \in \U)$

\Prop 33.43 $(x\in\dmn f \c \.fx \in \U)$

\Prop 33.44 $(x\in \dmn f \c \.fx \in \rng f)$

\Prop 33.45 $(y = \.fx \c y \in \rng f)$

\Prop 33.46 $(\ex \.fx\Iff \.fx \in \U)$

\Prop 33.47 $(\functionp f \And f \in \U \c \dmn f \in \U)$

\Prop 33.48 $(\dmn f \in \U \c f \in \U)$

\Prop 33.49 $(\dmn f \in \U \c f \in \function)$

\Prop 33.50 $(f \in \function \c \ex \dmn f)$

\Prop 33.51 $(f \in \function \c \ex \rng f)$

\Prop 33.52 $(\ex \dmn f \c \ex f)$

\Prop 33.53 $(\ex \rng f \c \ex f)$

\Prop 33.54 $(f \in \function \c \ex \rng f)$

\Prop 33.55 $(f \in \function \c \dmn f \in \U)$

\Prop 33.56 $(f \in \function \c \rng f \in \U)$

\Prop 33.57 $(f \in \function \c \functionp f)$

\Prop 33.58 $(f \in \onetoone \c f \in \function)$

\Prop 33.59 $(f \in \onetoone \And \.fa = \.fb \c a = b)$

\Prop 33.60 $(f\in\onetoone\And \ex\.fa \And\ex\.fb
\And a \ne b\c \.fa \ne \.fb)$

\Prop 33.61 $(f\in\onetoone\And a,b,\ne,\in\dmn f
\c \.fa,\.fb,\ne,\in\rng f)$

\Prop 33.62 $(f\in\onetoone\And a,b,\ne,\in\dmn f
\c \.fa\ne\.fb)$

\Prop 33.63 $(f\in\onetoone\And a,b,c,\ne,\in\dmn f
\c \.fa,\.fb,\.fc,\ne,\in\rng f)$

\Prop 33.64 $(f\in \function \And \Not(f \in \onetoone)
\c \Some x,y (x\ne y \And \.fx = \.fy))$

\Prop 33.65 $(f\in \function \And \Not(f \in \onetoone)
\c \Some x,y,\in\dmn f (x\ne y \And \.fx = \.fy))$

%\Prop 9.252 $(f \in \function \And \dmn f \in \totallyordered
%\And f \notin \onetoone \c \Some x,y (x < y \And \.fx = \.fy))$

\Prop 33.66 $\Not \. \Nul : A \into B$

\Prop 33.67 $(\.f : A \into B \And A \in \U \c f \in \U)$

\Prop 33.68 $(\functionp f \c f = \lonzo x \.fx)$

\Prop 33.69 $(f \in \function \c f = \lonzo x \.fx)$

\Prop 33.70 $(f \in \function \c \lonzo x \.fx = f)$

\Prop 33.71 $\functionp \lonzo x \ubar x$

\Prop 33.72 $(T \ident \lonzo x;\pbar x \ubar x \c \functionp T)$

\Prop 33.73 $(\functionp T\c \dmn T = \setof x \ex\.Tx)$

\Prop 33.74 $(T\in\function \c \dmn T=\setof x \ex\.Tx)$

\Prop 33.75 $(T \in \function \And y \in \rng T\c \Some x(\.Tx = y))$

\Prop 33.76 $(y \in \rng T \c \Some x (\.Tx = y))$

\Prop 33.77 $(y \in \rng T \c \Some x \in \dmn T(\.Tx = y))$

\Prop 33.78 $(T\ident\lonzo x\ubar x\c\dmn T=\setof x(\ubar x\in\U))$

\Prop 33.79 $(\Each x (\ubar x \ident \vbar x)\c
\lonzo x \ubar x \ident \lonzo x \vbar x)$

\Prop 33.80 $(f \ident \lonzo x \in A \ubar x \And \Each x \in A(\ubar x \in\U)
\And \ex A \c \dmn f = A)$

\Prop 33.81 $(f \ident \lonzo x \in A \ubar x \And \Each x \in A\ex\.fx
\And \ex A
\c \dmn f = A)$

\Prop 33.82 $(f \in \function \And \ex A\c
\ex \lostar fA)$

\Prop 33.83 $(\lostar f \{x\} = \{\.fx\}\Iff 
\functionp f \And x \in \dmn f)$

\Prop 33.84 $(f\in\function \c\lostar f\{x\}=\{\.fx\}
\Iff x \in\dmn f)$

\Prop 33.85 $(f\in\function \And A \i B
\c \lostar fA \i \lostar fB)$

\Prop 33.86 $(\ex \lostar f A \Iff \functionp f \And \ex A)$

\Prop 33.87 $(y \in \lostar f A \Iff \Some x \in A(y = \.f x))$

\Prop 33.88 $(\ex \lostar f A \Iff \lostar f A \i \rng f)$ 

\Prop 33.89 $(f \in \function \And\ex A\c\lostar f A \i \rng f)$ 

\Prop 33.90 $(f\in\function \c \ex\lostar fA \Iff \ex A)$

\Prop 33.91 $( x \notin \rng b \And x \in \U \c  \histar b \{x\}=\e )$ 

\Prop 33.92 $(\lostar f(A\cup B)\ident\lostar fA\cup\lostar fB)$

\Prop 33.93 $(\functionp f \And \functionp g \And \dmn f \cap \dmn g = \e \c \functionp(f\cup g))$

\Prop 33.94 $(A\ne \e \c
\lostar f \bigcup x \in A \ubar x \ident \bigcup x\in A\lostar 
f \ubar x)$

\Prop 33.95 $(f\in\function\c
\lostar f \bigcup x \in A \ubar x \ident \bigcup x\in A\lostar 
f \ubar x)$

\Prop 33.96 $(\Each x( \pbar x \c \ex \lostar f \vbar x) 
\c \lostar f \bigcup x ; \pbar x \vbar x = \bigcup x;\pbar x \lostar f \vbar x)$

\Prop 33.97 $(b \in \function \c \ex \histar b A \Iff \ex A)$

\Prop 33.98 $(b\in\function \c \histar bA\in \U \Iff \ex\histar bA)$

\Prop 33.99 $(b\in\function \c \histar bA\in \U \Iff \ex  A)$

\Prop 33.100 $(b\in\function  \And B = \histar bA\c B \i \dmn b)$

\Prop 33.101 $(b \in \function \c \histar bA \i\dmn b\Iff \ex A)$

\Prop 33.102 $(b \in \function \And A\in\U\And B\in \U
\c \histar b (A \cap B) = \histar bA \cap \histar bB)$

\Prop 33.103 $(f \in \function \c \histar f(A \cap B) \ident \histar fA \cap\histar fB)$

\Prop 33.104 $(f \in \function \c \histar f(A \cup B) \ident \histar fA \cup\histar fB)$

\Prop 33.105 $(f \in \function \c \histar fA \cap\histar fB \ident \histar f(A \cap B) )$

\Prop 33.106 $(f \in \function \c \histar fA \cup\histar fB \ident \histar f(A \cup B) )$

\Prop 33.107 $(\ex \histar fA \c \ex A)$

\Prop 33.108 $(f\in\function \c \histar f\e = \e)$

\Prop 33.109 $(b \in \function \c
x \in \histar bA \Iff \.bx \in A)$

\Prop 33.110 $(\.bx \in A \c x \in \histar bA)$

\Prop 33.111 $(\rng f \i A \c \dmn f = \histar fA)$

\Prop 33.112 $(y = \.bx \And z \notin \rng b\c y \ne z)$ 

\Prop 33.113 $(f = \{(a,b)\} \c f \in \function)$ 

\Prop 33.114 $(f = \{(a,b)\} \c \dmn f = \{a\})$

\Prop 33.115 $(f = \{(a,b)\} \c \rng f = \{b\})$

\Prop 33.116 $(f = \{(a,b)\} \c \.fa =  b)$

\Prop 33.117 $(f = \{(a,b),(c,d)\} \And a \ne c\c f \in \function)$ 

\Prop 33.118 $(f = \{(a,b),(c,d)\} \And a \ne c\c \dmn f = \{a,c\})$

\Prop 33.119 $(f = \{(a,b),(c,d)\} \And a \ne c\c \rng f = \{b,d\})$

\Prop 33.120 $(f = \{(a,b),(c,d)\} \And a \ne c\c \.fa =  b)$

\Prop 33.121 $(f = \{(a,b),(c,d)\} \And a \ne c\c \.fc =  d)$

\Prop 33.122 $(\dmn f \in \U \And \Each x,y(\.fx = \.fy \c x = y) \c  f \in \onetoone)$

\Prop 33.123 $(\dmn f = \e \c f \in \onetoone)$

\Prop 33.124 $(\rng f \i A \And \ex x \c \vs fx \i A)$

\Prop 33.125 $(\dmn f \i A \And \ex y \c \hs fy \i A)$

\Prop 33.126 $(A = \rng f \And \ex x \c \vs fx \i A)$

\Prop 33.127 $(A = \dmn f  \And \ex y \c \hs fy \i A)$

\Prop 33.128 $(f \in \function \c \.fx = y \Iff x \in \hs fy)$

\Prop 33.129 $(f \in \function \c x \in \hs fy \Iff \.fx = y )$

\Prop 33.130 $(f \in \function \c \ex \hs fx \Iff \ex x)$

\Prop 33.131 $(f \in \function \c \ex \vs fx \Iff \ex x)$

\Prop 33.132 $(\relationp f \And \Each x \Unq y ((x,y) \in f) \c \functionp f)$

\Prop 33.133 $(\relationp f \And \Each x \in \Dmn f \Unq y ((x,y) \in f) \c \functionp f)$

\Prop 33.134 $(\functionp f \And g \i f \c \functionp g)$

\Prop 33.135 $(\functionp f \And (x, a) \in f \And (x,b) \in f \c a = b)$

\Prop 33.136 $(\functionp f \And \dmn f = A \And \rng f \i B\c \. f : A \into B )$

\Prop 33.137 $(\. f : A \into B \c \functionp f )$

\Prop 33.138 $(\. f : A \into B \c A = \dmn f )$

\Prop 33.139 $(\. f : A \into B \c \rng f \i B)$



\noindent{Theorems}

\Prop 33.141 $(\histar f(A \cup B) \ident \histar fA \cup \histar fB)$

\Prop 33.142 $(f\in\function \And \ex B \c \lostar f\histar f B \i B)$

\Prop 33.143 $(f \in \function \c \lostar f \dmn f = \rng f)$

\Prop 33.144 $(f \in \function \And A\i B \c \lostar fA \i \lostar fB)$

\Prop 33.145 $(f \in \function \And A\i B \c \histar fA \i \histar fB)$

\Prop 33.146 $(f \in \function \c \histar f \rng f = \dmn f)$

\Prop 33.147 $(z \in \onetoone \And \ex A \And \ex B \c 
	\lostar z(A \cap B) = \lostar zA \cap \lostar zB)$

\Prop 33.148 $(z \in \onetoone \And \Each x;\pbar x \ex \ubar x 
	\And \Some x \pbar x $
 $\c
	\bigcap x;\pbar x \lostar z \ubar x = \lostar z \bigcap x;\pbar x \ubar x)$

\Prop 33.149 $(z \in \onetoone \And \ex A \And \ex B \c 
	\lostar z(A \setdif B) = \lostar zA \setdif \lostar zB)$

\Prop 33.150 $(\dmn f = A \And \dmn g = A \And \Each x \in A (\.fx = \.gx)\c f=g)$

\Prop 33.151 $(A \i \dmn f \And x \in A \c \.\strc fA x = \.fx)$

\Prop 33.152 $(A \i B \And \functionp f \c \strc f A \i \strc f B)$

\Prop 33.153 $(A \i \dmn f \And A \i\dmn g \c \strc f A = \strc g A \Iff \Each x \in A(\.fx = \.gx))$

\Prop 33.154 $(A \i \dmn f \And A \i\dmn g \And \strc f A = \strc g A \c \Each x \in A(\.fx = \.gx))$

\Prop 33.155 $(A \i \dmn f \And A \i\dmn g \And \Each x \in A(\.fx = \.gx) 
\c \strc f A = \strc g A )$

\Prop 33.156 $(f \i g \And \functionp g \And \dmn f = A \c f = \strc g A)$

\Prop 33.157 $(f \i g \And \functionp g \c \functionp f)$

\Prop 33.158 $(\functionp f \And g = \strc f A \c g \i f)$

\Prop 33.159 $(\functionp f \And g = \strc f A \c \functionp g)$ 

\Prop 33.160 $(\functionp f \And g \ident \strc f A \c \ex g \Iff \ex A)$

\Prop 33.161 $(\functionp f \And g \ident \strc f A \And \ex A \c \ex g)$

\Prop 33.162 $(\functionp f \And g \ident \strc f A \And \ex A \c \functionp g)$

\Prop 33.163 $(\functionp f \And g \ident \strc f A \And A \i \dmn f\c \dmn g = A)$

\Prop 33.164 $(\functionp f \c \Dmn f = \dmn f)$

\Prop 33.165 $(\functionp f \And g \ident \strc f A \And \ex A \c g = \strc fA)$

\Prop 33.166 $(f \ident \lonzo x ;\pbar x \ubar x \c (a,b) \in f \Iff a,b, \in \U 
\And \pbar a \And b = \ubar a)$

\Prop 33.167 $(f \ident \lonzo x ;\pbar x \ubar x \And a,b, \in \U 
\And \pbar a \And b = \ubar a \c (a,b) \in f)$

\Prop 33.168 $(f \ident \lonzo x ;\pbar x \ubar x \And (a,b) \in f \c a,b, \in \U 
\And \pbar a \And b = \ubar a)$

\Prop 32.336 $(R \i S \And \functionp S \c \rng R \i \rng S)$

\Prop 32.10 $(A \i B \And \functionp R \c \strc RA \i \strc RB)$

\lineb

\chap{34. Function Builder Unwrapping Theorems} 
	\lineb

\prop 34.1 $\ex \lonzo x \ubar x$

\prop 34.2 $(f \ident \lonzo x \ubar x \c f = \lonzo x \ubar x)$

\prop 34.3 $(f \ident \lonzo x \ubar x \c y = \.fx \Iff y = \ubar x \And 
	x \in \U \And y \in \U)$

\prop 34.4 $(f \ident \lonzo x \ubar x \c \functionp f)$

\prop 34.5 $(f \ident \lonzo x \ubar x \c \dmn f = \setof x (\ubar x \in \U))$

\prop 34.6 $(f \ident \lonzo x \ubar x 
	\And \Each x(\ex \ubar x \c \ubar x \in \U) 
	\c y = \.fx \Iff y = \ubar x \And x \in \U)$

\prop 34.7 $(f \ident \lonzo x \ubar x 
	\And \Each x(\ex \ubar x \c \ubar x \in \U) \And y \in \U
	\c \.fy \ident \ubar y )$

\prop 34.8 $(f \ident \lonzo x \ubar x
	\And\Each x(\ex \ubar x \c \ubar x \in \U \And x \in \U) \And 
	\Not \ex \ubar \Nul \c \.fy \ident \ubar y)$

\prop 34.9 $(f \ident \lonzo x\in A  \ubar x
	\And\Each x \in A (\ubar x \in \U ) \And y \in A
	 \c \.fy = \ubar y)$

\Prop 34.10 $(f \ident \lonzo x\in A  \ubar x
	\And\Each x \in A (\ex \ubar x \c \ubar x \in \U ) \And y \in A
	 \c \.fy \ident \ubar y)$

\Prop 34.11 $(f \ident \lonzo x\in A;\pbar x  \ubar x
	\And\Each x \in A;\pbar x (\ex \ubar x \c \ubar x \in \U ) \And y \in A \And \pbar y
	 \c \.fy \ident \ubar y)$

\Prop 34.12 $(f \ident \lonzo x\in A;\pbar x  \ubar x
	\And\Each x \in A;\pbar x (\ubar x \in \U ) \And y \in A \And \pbar y
	 \c \.fy \ident \ubar y)$

\Prop 34.13 $(f \ident \lonzo x,y \in A  \ubarp xy
	\And\Each x,y \in A (\ex \ubarp xy \c \ubarp xy \in \U ) \And (u,v) \in A
	 \c \.f(u,v) \ident \ubarp uv)$

\Prop 34.14 $(f \ident \lonzo x\in A  \ubar x
	\And\Each x \in A (\ubar x \in \U ) \And \ex A \c \dmn f = A)$

\Prop 34.15 $(f \ident \lonzo x \in A \ubar x \And\ex A \c \dmn f \i A)$

\Prop 34.16 $(f \ident \lonzo x,y \in A \ubarp xy \And\ex A \c \dmn f \i A)$

\Prop 34.17 $(f \ident \lonzo x,y\in A \ubarp xy \And \Not\ex A \c \dmn f = \e)$

\Prop 34.18 $(f \ident \lonzo x \in A \ubar x
\c \dmn f = \setof  x \in A (\ubar x \in \U ))$

\Prop 34.19 $(f \ident \lonzo x \in A \ubar x
\c \rng f = \setof  \ubar x  \ls x \in A \rs)$

\Prop 34.20 $(f \ident \lonzo x,y \in A \ubarp xy
\c \rng f = \setof  \ubarp xy  \ls x,y \in A \rs)$

\Prop 34.21 $(f \ident \lonzo x\in A  \ubar x
\And\Each x \in A (\ubar x \in \U )\And \ex A  \c \rng f = \setof \ubar x \ls x \in A \rs)$

\Prop 34.22 $(f \ident \lonzo x,y \in z \ubarp xy \And g \ident f \c g = f)$
	\lineb

\noindent{\bf Conditionals and the Function Builder}
	\lineb

\Prop 34.23 $(f \ident (\pvar \cond \lonzo x \ubar x) 
		\c \ex f \Iff \pvar)$

\Prop 34.24 $(f \ident (\pvar \cond \lonzo x \ubar x) 
		\c \pvar \Iff f = \lonzo x \ubar x)$

\Prop 34.25 $(f \ident (\pvar \cond \lonzo x \ubar x)
	\c y = \.fx \Iff \pvar \And y = \ubar x \And x \in \U \And y \in \U)$

\Prop 34.26 $(f \ident (\pvar \cond \lonzo x \ubar x) 
	\And \Each x(\ex \ubar x \c \ubar x \in \U) 
	\c y = \.fx \Iff \pvar \And y = \ubar x \And x \in \U)$

\Prop 34.27 $(f \ident (\pvar \cond \lonzo x \ubar x) 
	\And \Each x (\ex \ubar x \c \ubar x \in \U \And x \in \U) \And 
	\Not \ex \ubar \Nul \c y = \.fx \Iff \pvar \And y = \ubar x)$
	\lineb

\noindent{\bf The Function Builder with Cases}
\lineb

Constructions sometimes involve defining functions by cases.  The
variety of possibilities here is large, but the following list of
unwrapping theorems gives the flavor.
	\lineb

\Prop 34.28 $(f \ident \lonzo x \in A (\pbar x \cond \ubar x \els \vbar x) \And
\Each x \in A (\pbar x \c \ubar x \in \U) \And y \in A \And \pbar y \c \.fy = \ubar y)$ 

\Prop 34.29 $(f \ident \lonzo x \in A (\pbar x \cond \ubar x \els \vbar x) \And
\Each x \in A(\Not \pbar x \c \vbar x \in \U)\And y \in A \And\Not\pbar y\c\.fy = \vbar y)$ 


\Prop 34.30 $(f \ident \lonzo x \in A (\pbar x \cond \ubar x \els \vbar x) \And
\Each x \in A(\pbar x \c \ubar x \in \U)\And
\Each x \in A(\Not \pbar x \c \vbar x \in \U) \c \dmn f = A)$

\Prop 34.31 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
\Each x \in A (\ubar x \in \U) \And y \in A \c \.fy = \ubar y)$ 

\Prop 34.32 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
A \cap B = \e \And \Each x \in B (\vbar x \in \U) \And y \in B \c \.fy = \vbar y)$ 

\Prop 34.33 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
\Each x \in B \setdif A(\vbar x \in \U) \And y \in B \setdif A \c \.fy = \vbar y)$ 

\Prop 34.34 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
\Each x \in A(\ubar x \in \U) \And \Each x \in B (\vbar x \in \U) \c \dmn f = A \cup B)$ 

\Prop 34.35 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
\Each x \in A(\ubar x \in \U) \And \Each x \in B\setdif A (\vbar x \in \U) \c \dmn f = A \cup B)$ 

\Prop 34.36 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
 \dmn f = A \cup B \And A \cap B = \e \And y \in A \c \.fy = \ubar y)$ 

\Prop 34.37 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \And
 \dmn f = A \cup B \And A \cap B = \e \And y \in B \c \.fy = \vbar y)$ 

\Prop 34.38 $(f \ident \lonzo x (x \in A \cond \ubar x \els x \in B \cond \vbar x) \c
 \dmn f \i A \cup B \Iff \ex(A\cup B))$ 
	\lineb

\Prop 34.39 $(f \ident \lonzo x (\ubar x \case \vbar x) \And 
\Each x \Not(\ex \ubar x \And \ex \vbar x) \c \rng f = \rng \lonzo x \ubar x \cup
\rng \lonzo x \vbar x)$

\Prop 34.40 $(f \ident \lonzo x (\ubar x \case \vbar x) \And 
\Each x \Not(\ex \ubar x \And \ex \vbar x) \c \dmn f = \setof x (\ubar x \in \U \Or \vbar x \in \U))$

\Prop 34.41 $(f \ident \lonzo x (\ubar x \case \vbar x) \And 
\Each x \Not(\ex \ubar x \And \ex \vbar x) \And \ubar y \in \U \c \.fy = \ubar y)$


\Prop 34.42 $(f \ident \lonzo x (\ubar x \case \vbar x) \And 
\Each x \Not(\ex \ubar x \And \ex \vbar x) \And \vbar y \in \U \c \.fy = \vbar y)$
	\lineb

	\vfill\eject

\chap{35. Spaces}
\lineb

When sets are endowed with a structure such as an ordering
or a multiplication, the need for a definition of such an 
endowment is usually given token acknowledgement using 
a tuple.  For example an ordered set might be defined as
a pair  $(X,R)$ where $R$ is an ordering on $X$,  or a set
with a multiplication as a pair $(X, b)$ where $b$ is
a binary operation on $X$.  Little use is actually made of such 
definitions.  Indeed it is doubtful that any use could be made
of them in a formal development without giving up almost entirely
on the use of notations such as `$(x \le y)$' or `$(x \cdot y)$'.  
This appendix outlines some ideas aimed at retaining these
traditional notations without any sacrifice in formality.  
 
In order to give fixed definitions to these notations
we require that the structure referred by them to be bundled into
the operands.   Thus in order to perform the comparison operation
$(x \le y)$ an order operation carried by $x$ or $y$ is used. 
Similarly a multiplication $(x \cdot y)$ accesses a multiplication
carried by $x$ or $y$.  Consequently, $x$ and $y$ if they are
to be compared or multiplied must become ``structure carriers.''
To implement this idea we require that $x$ and $y$ be functions
whose domain consists of ``name tags,'' one for each structure
carried as well as the empty set which tags the unadorned element 
itself.  
\lineb

\noindent{\bf{The Name Tag Alphabet}}\vskip 2pt
\lineb

The purpose of the definitions below is to establish an 
alphabet for use forming name tags. 
The first 26 successors of the empty set are defined as
``letters'' which can be combined in tuples to ``spell'' the name tags.
For example in 38.1, we define the tag
\noparse $\underl{plus}$ as $(\dbar p, \dbar l, \dbar u, \dbar  s))$.
Similarly in 39.1 below we see that the tag for
the multiplication symbol \noparse `$\cdot$' is
the tuple 
\noparse $(\dbart, \dbari, \dbarm , \dbare ,\dbars)$ which we denote by `$\ultimes$.'  
Thus if $x$ is the element of an ordered field, then $x$ is a function
whose domain must include at least the four elements 
\noparse $\{\e, \underl{plus},\ultimes,\underl{lessthan}\}$.
\lineb



\noindent{{Definitions}}\vskip 2pt

\prop 35.1 $(\scsr x \ident x \cup \{x\})$

\prop 35.2 $(\dbara \ident \scsr \e)$

\prop 35.3 $(\dbarb\ident \scsr \dbara)$

\prop 35.4 $(\dbarc\ident \scsr \dbarb)$

\prop 35.5 $(\dbard\ident \scsr \dbarc)$

\prop 35.6 $(\dbare\ident \scsr \dbard)$

\prop 35.7 $(\dbarf\ident \scsr \dbare)$

\prop 35.8 $(\dbarg\ident \scsr \dbarf)$

\prop 35.9 $(\dbarh\ident \scsr \dbarg)$

\Prop 35.10 $(\dbari\ident \scsr \dbarh)$

\Prop 35.11 $(\dbarj\ident \scsr \dbari)$

\Prop 35.12 $(\dbark\ident \scsr \dbarj)$

\Prop 35.13 $(\dbarl\ident \scsr \dbark)$

\Prop 35.14 $(\dbarm\ident \scsr \dbarl)$

\Prop 35.15 $(\dbarn\ident \scsr \dbarm)$

\Prop 35.16 $(\dbaro\ident \scsr \dbarn)$

\Prop 35.17 $(\dbarp\ident \scsr \dbaro)$

\Prop 35.18 $(\dbarq\ident \scsr \dbarp)$

\Prop 35.19 $(\dbarr\ident \scsr \dbarq)$

\Prop 35.20 $(\dbars\ident \scsr \dbarr)$

\Prop 35.21 $(\dbart\ident \scsr \dbars)$

\Prop 35.22 $(\dbaru\ident \scsr \dbart)$

\Prop 35.23 $(\dbarv\ident \scsr \dbarr)$

\Prop 35.24 $(\dbarw\ident \scsr \dbarv)$

\Prop 35.25 $(\dbarx\ident \scsr \dbarw)$

\Prop 35.26 $(\dbary\ident \scsr \dbarx)$

\Prop 35.27 $(\dbarz\ident \scsr \dbary)$
\lineb

\chap{36. Basic Structure Carrying Definitions}
\lineb

Definition 36.1 below defines a space as a set of elements all of
which carry exactly the same structure.  In 36.2 the underlying set
of a space is defined.  In 36.4 we have a define the structure that 
in the space $S$ is associated with the name tag $t$. 

\lineb


\prop 36.1 $(\Space \ident \setof A \i \function
\Each x \in A (\e \in \dmn x \And \Each y \in A
(\strc x \Cmpl \{\e\} = \strc y \Cmpl \{\e\})))$

\prop 36.2 $(\Set A \ident (A \in \Space\cond \setof \.x\e\ls x \in A \rs ))$

\prop 36.3 $(\structdmn S \ident (S \in \Space \cond \Case x \in S 
	(\dmn x \setdif \{\e\})))$


\prop 36.4 $(\Struct St \ident (t \in \structdmn S \cond \Case x \in S \.xt))$


\lineb

\chap{37. Partial Order Relations}
\lineb


\noindent{Definitions}

\prop 37.1 $(\transitive \ident \setof R \in \relation
\Each x,y,z ((x,y)\in R \And (y,z)\in R\c (x,z)\in R))$

\prop 37.2 $(\antisymmetric \ident \setof R \in \relation
\Each x,y ((x,y) \in R \And (y,x) \in R \c x = y))$
 
\prop 37.3 $(\underl{lessthan} \ident
(\dbarl, \dbare, \dbars, \dbars, \dbart, \dbarh, \dbara, \dbarn))$

\prop 37.4 $((x \le y) \Iff \Some R = \Struct \{x,y\} \underl{lessthan}
	( R \in \transitive \And R \in \antisymmetric \And $
\linee $((\.x \e , \.y\e) \in R \Or x=y)))$

\prop 37.5 $(\orderedset \ident \setof X \in \Space \Each x \in X(x \le x))$

\prop 37.6 $((x < y) \Iff (x \le y \And x \ne y))$

\prop 37.7 $((x \ge y) \Iff (y \le x))$

\prop 37.8 $((x > y) \Iff (y < x))$

\prop 37.9 $(\lbrack a,b \rbrack \ident (a \le b \cond
\setof t(a \le t \And t \le b)))$

\Prop 37.10 $(\langle a,b \rangle \ident (a \le b \cond
\setof t(a < t \And t < b)))$

\Prop 37.52 $(\Max A \ident \The x \in A \Each y \in A(y \le x))$

\Prop 37.53 $(\Min A \ident \The x \in A \Each y \in A(y \ge x))$
	\lineb
In this section we define $(x \le y)$ so that it works by virtue  
of a partial order relation carried by both $x$ and $y$.  Note
that whether this relation is reflexive or not does not affect 
whether we have $(x \le x)$ or not.  The notation is overriding
here.
In 37.5 we define an ordered set as a space whose elements all 
carry the same partial order relation.  

We assume that the natural numbers $\nats$ and the
integers $\ints$ have been constructed
in such a way that $(\nats,\ints,\in\orderedset)$.\footnote*{Additionally
we assume that $(\nats\i\ints)$. Satisfying these requirements
simultaneously is nontrivial.} 

\lineb

Note that by requiring the structure tagged by $\underl{lessthan}$
to be a partial ordering and that it be shared by both terms
related, we can state following fully self-contained
theorems.
	\lineb

\noindent{Theorems}


\Prop 37.11 $(x < y \c \ex x)$

\Prop 37.12 $(x < y \c \ex y)$

\Prop 37.13 $(x \le y \c \ex x)$

\Prop 37.14 $(x \le y \c \ex y)$

\Prop 37.15 $(a > b \c \ex a)$

\Prop 37.16 $(a > b \c \ex b)$

\Prop 37.17 $(x \ge y \c \ex x)$

\Prop 37.18 $(x \ge y \c \ex y)$

\Prop 37.19 $(x \le y \c x \le x )$

\Prop 37.20 $(x \le y \c y \le y )$

\Prop 37.21 $(x \le y \And y \le z \c x \le z)$

\Prop 37.22 $(x \le y \And y < z \c x < z)$

\Prop 37.23 $(x < y \And y \le z \c x < z)$

\Prop 37.24 $(x < y \And y < z \c x < z)$

\Prop 37.25 $(x < y \c x \le y)$

\Prop 37.26 $(x < y \c x \ne y)$

\Prop 37.27 $(x \le y \And x \ne y \c x < y)$

\Prop 37.28 $(x \le y \And y \le x \c x = y)$

\Prop 37.29 $(x \ge y \And y \ge z \c x \ge z)$

\Prop 37.30 $(x > y \And y > z \c x > z)$

\Prop 37.31 $(x \ge y \And y > z \c x > z)$

\Prop 37.32 $(x > y \And y \ge z \c x > z)$

\Prop 37.33 $(x > y \c x \ge y)$

\Prop 37.34 $(x > y \c x \ne y)$

\Prop 37.35 $(x \ge y \And x \ne y \c x > y)$

\Prop 37.36 $(x \ge y \And y \ge x \c x = y)$

\Prop 37.37 $(x \le y \c \Not(x > y))$

\Prop 37.38 $(x < y \c \Not(x \ge y))$

\Prop 37.39 $(x > y \c \Not(x \le y))$

\Prop 37.40 $(x \ge y \c \Not(x < y))$

\Prop 37.41 $(x < y \Iff y > x)$

\Prop 37.42 $(x \le  y\Iff y \ge x)$

\Prop 37.43 $(x = \Max A \c x \in A)$

\Prop 37.44 $(x = \Min A \c x \in A)$

\Prop 37.45 $(x = \Max A \c \Each y \in A(y \le x))$

\Prop 37.46 $(x = \Max A \And y \in A \c y \le x)$

\Prop 37.47 $(x = \Min A \c \Each y \in A (y \ge x))$

\Prop 37.48 $(x = \Min A \And y \in A \c y \ge x)$

\Prop 37.49 $(x = \Min A \And y \in A \c x \le y)$

\Prop 37.50 $(x = \Min A \And y < x \c y \notin A)$

\Prop 37.51 $(x = \Max A \And y > x \c y \notin A)$

\lineb

\chap{38. Using Plus for Operations which are Commutative and Associative}
\lineb

\prop 38.1 $(\ulplus \ident (\dbarp, \dbarl, \dbaru, \dbars))$


Let $S$ be a non-empty set and let
\noparse $\.f: S \lilx S \into S$ be a commutative and associative operation on $S$
which we seek to denote using the plus sign.
To do this we create a space $X$ whose elements are functions and whose domain
\noparse is the set $\{\e, \ulplus\}$.  For all these functions $(x\in X)$ it is true that
$(\.x\e \in S)$ and  $(\.x\ulplus = f)$.
In fact we may let 
\lineb

$(X \ident \setof \{(\e,s),(\ulplus,f)\}\ls s \in S\rs)$
\lineb

\noindent{}The operation $(x + y)$ 
produces the following element of the space
\lineb 

$(x + y = \{(\e, \.f (\.x \e,\.y \e)), (\ulplus,f)\})$
\lineb


\lineb In definition 38.6 below we require that  
in order for 
$(x + y)$
to be defined both $x$ and $y$ must carry the identical structure.
This is done by stipulating that $(\{x,y\} \in \Space)$.
The assignment 
\lineb

$(f = \Struct\{x,y\}\ulplus)$ 
\lineb

\noindent{}picks out the structure associated with the plus name tag
carried by both $x$ and $y$.
\lineb

\noindent{{Definitions}}

\prop 38.2 $(\commutative \ident \setof f \in \function \Each x,y
(\.f(x,y) \ident \.f(y,x)))$

\prop 38.3 $(\associative \ident \setof f \in \function \Each x,y,z
(\.f(x,\.f(y,z)) \ident \.f(\.f(x,y),z)))$

\prop 38.4 $(\ulplus \ident (\dbarp, \dbarl, \dbaru, \dbars))$

\prop 38.5 $(\addops az \ident (\{(\e,a)\} \cup \strc z \Cmpl \{\e\}))$

\prop 38.6 $((x + y) \ident \Case f = \Struct \{x,y\}\ulplus $
\linec $(f \in \commutative \And f \in \associative \cond $
	 $\addops \.f(\.x\e, \.y\e) y))$

\prop 38.7 $((x + y + z) \ident ((x + y) + z))$
\lineb

\noindent{{Theorems}}


\prop 38.8 $(a + b \ident b + a)$

\prop 38.9 $((a + b) + c \ident a + (b + c))$
\lineb

\noindent{Other Theorems}

\Prop 38.10 $((a + b) + c \ident a + b + c)$

\Prop 38.11 $((a + b) + c \ident a + (b + c))$

\Prop 38.12 $(a + (b + c) \ident a + b + c)$

\Prop 38.13 $(a + b + c \ident a + c + b)$

\Prop 38.14 $(a + b + c \ident b + a + c)$

\Prop 38.15 $(\ex(a + b) \c \ex a)$

\Prop 38.16 $(\ex(a + b) \c \ex b)$

\Prop 38.17 $(\ex(a + b + c) \c \ex a)$

\Prop 38.18 $(\ex(a + b + c) \c \ex b)$

\Prop 38.19 $(\ex(a + b + c) \c \ex c)$
\lineb

\noindent{\bf{Partially Defined Additive Inverses}}
\lineb

When plus and minus signs are mixed in one expression, we may
use the commutative and associative properties to reduce the
expression to a single difference operation, which may or may
not be defined. 

\Prop 38.20 $(a + b - c \ident (a + b) - c)$

\Prop 38.21 $((a + b) - c \ident a + b - c)$

\Prop 38.22 $(a - b - c \ident a - (b + c))$ 

\Prop 38.23 $(a - (b + c) \ident a - b - c)$

\Prop 38.24 $(a + b + c - d \ident (a + b + c) - d)$

etc.
\lineb

\chap{39. Using Times for Inhomogenous Operations which are Associative}
\lineb

Implementing a multiplication constant is complicated by the fact that
multiplication often occurs between heterogeneous objects. In scalar multiplication
of vectors for example the multiplication carried by the $\lambda$ itself
in $(\lambda \cdot x)$ may be restricted to a field such as the field of
real numbers and we should not  require it to handle  the multiplication of
vectors.  Hence we must obtain the multiplication to be used from
the vector $x$ not the scalor $\lambda$.  
To solve this problem we require that the multiplication operation carried
by the vector includes the scalor field multiplication.  That way
we can easily identify the larger of the two operand domains.  We use the
multiplication from the larger and require that both operands ``lean'' in
the same direction. 


\noindent{{Definitions}}

%precedence= 19
%primitive_term: (a \_ b) 

\prop 39.1 $(\ultimes \ident (\dbart, \dbari, \dbarm, \dbare, \dbars))$

\prop 39.2 $(\Proj xA \ident \setof (a\_ x)\ls a \in A\rs)$

\prop 39.3 $((x \cdot y) \ident \Case f = \Struct \{x\}\ultimes 
\Case g = \Struct\{y\}\ultimes ($
\linec$ \Proj 0\dmn f  \i \Proj 1\dmn f \And $
$\Proj0\dmn g \i \Proj1\dmn g\And f \i g \And g \in \associative $
\linee$\cond \addops \.g(\.x\e,\.y\e)y \els$
\linec$ \Proj 1\dmn f \i  \Proj 0\dmn f \And \Proj 1\dmn g\i \Proj 0\dmn g\And g \i f \And $
$ f \in \associative $
\linee$\cond \addops \.f(\.x\e,\.y\e)x))$

\prop 39.4 $((x \cdot y \cdot z) \ident ((x \cdot y) \cdot z))$
\lineb

\noindent{Theorem}

\prop 39.5 $(x \cdot (y \cdot z) \ident (x \cdot y) \cdot z)$
\lineb

\noindent{Other Theorems}

\prop 39.6 $(a \cdot b \cdot c \ident a \cdot (b  \cdot c))$

\prop 39.7 $(a \cdot (b \cdot c) \ident (a \cdot b) \cdot c)$

\prop 39.8 $((a \cdot b) \cdot c \ident a \cdot (b \cdot c))$

\prop 39.9 $((a \cdot b) \cdot c \cdot d\ident a \cdot (b \cdot c)\cdot d)$

\Prop 39.10 $(a \cdot b \cdot c \cdot d\ident a \cdot (b \cdot c) \cdot d)$ 

\Prop 39.11 $(a \cdot b \cdot c \cdot d\ident a \cdot b \cdot (c \cdot d))$ 

\Prop 39.12 $(a \cdot (b \cdot c) \cdot d\ident a \cdot b \cdot (c \cdot d))$ 

\Prop 39.13 $(a \cdot b \cdot c \cdot d\ident (a \cdot b) \cdot c \cdot d)$ 

\Prop 39.14 $(a \cdot (b \cdot c) \cdot d\ident (a \cdot b) \cdot c \cdot d)$ 

\Prop 39.15 $(\ex (a \cdot b) \c \ex a)$

\Prop 39.16 $(\ex (a \cdot b) \c \ex b)$
\lineb





\chap{40. Natural Numbers}


\Prop 40.100 $( 0 \ident \The x \in \nats (\.x\e = \e))$

\Prop 40.101 $((a \_ b) \ident ((b \in \nats) \cond a \_ \.b\e \els a \_ b))$

\prop 40.1 $(0 \in \nats)$

\prop 40.2 $\ex 0$

\prop 40.3$\Some x (x \in\nats)$

\prop 40.4 $(1 \in \nats)$

\prop 40.5 $\ex 1$

\prop 40.6 $( 1 \ne 0)$

\prop 40.7 $( 2 \ne 1)$

\prop 40.8 $(2 \in \nats)$

\prop 40.9 $(3 \in \nats)$

\Prop 40.10 $(n \in \nats \c  n + 0 = n)$

\Prop 40.11 $(n \in \nats \c  0 + n = n )$

\Prop 40.12 $(n \in \nats \c  n = n + 0 )$

\Prop 40.13 $(n \in \nats \c  n = 0 + n  )$

\Prop 40.14 $(n \in \nats \c n - 0 =n)$

\Prop 40.15 $(n \in \nats \c n - n =0)$

\Prop 40.16 $(n \in \nats \c 0 = n - n)$

\Prop 40.17 $(n \in \nats \c n + 1 \in \nats)$

\Prop 40.18 $(n\in\nats \c n \ne n-1)$

\Prop 40.19 $(n\in\nats \c n > n-1)$

\Prop 40.20 $(n\in\nats \c  n-1 < n)$

\Prop 40.21 $(n\in\nats \c n < n+1)$

\Prop 40.22 $(n\in\nats \c n+1 > n)$

\Prop 40.23 $(n\in\nats \c n \ne n+1)$

\Prop 40.24 $(n\in\nats \c  n+1 \ne n)$

\Prop 40.25 $(m,n, \in \nats \c m + n  \in \nats)$

\Prop 40.26 $(m,n,\in\nats \And m-1 = n-1 \c m = n)$

\Prop 40.27 $(m \in \nats \c m = 0 \Or\Some n \in\nats(m = n+1))$

\Prop 40.28 $(m \in \nats \c m = 0 \Or m > 0)$

\Prop 40.29 $(m \in \nats \And m > 0 \c m-1 \in \nats)$

\Prop 40.30 $(m \in \nats \And m \ne 0 \c m-1 \in \nats)$

\Prop 40.31 $(m \in \nats \c 0\le m)$

\Prop 40.32 $(m \in \nats \c m \ge 0)$

\Prop 40.33 $(M \i \nats \And 0 \in M \And \Each n \in M(n+1 \in M)
	\c M = \nats)$

\Prop 40.34 $(m,n,k, \in \nats \And m+k = n + k \c m = n)$ 

\Prop 40.35 $(n \in \nats \c n = 0 \Or \Some m \in \nats
(n = m + 1))$

\Prop 40.36 $(\nats \ne \e)$

\Prop 40.37 $\ex\nats$

\Prop 40.38 $(\nats \in \U)$

\Prop 40.39 $(m,n , \in \nats \And k = m + n \c k - n = m)$ 

\Prop 40.40 $(m,n , \in \nats \And k = m + n \c k - m = n)$ 

\Prop 40.41 $(n \in \nats \And n \le 0 \Iff n = 0)$

\Prop 40.42 $(n \in \nats \And n \le 1 \Iff n = 0 \Or n=1)$

\Prop 40.43 $(n \in \nats \And n \le 2\Iff n=0\Or n=1\Or n=2)$

\Prop 40.44 $(m,n,\in \nats \c m\cdot n \in \nats)$

\Prop 40.45 $(m \in \nats \c m \cdot 0 = 0)$

\Prop 40.46 $(m \in \nats \c 0 = m \cdot 0)$

\Prop 40.47 $(m \in \nats \c m \cdot 1 = m)$

\Prop 40.48 $(m \in \nats \c m = m \cdot 1)$

\Prop 40.49 $(m \in \nats \c m \cdot 2 = m + m)$

\Prop 40.50 $(m \in \nats \c m + m = m \cdot 2)$

\Prop 40.51 $(m,n,p, \in \nats \c (m + n) \cdot p = (m \cdot p) + (n \cdot p))$

\Prop 40.52 $(m,n,p, \in \nats \c (m \cdot p) + (n \cdot p) =  (m + n) \cdot p )$

\Prop 40.53 $(m,n,p, \in \nats \c p \cdot (m + n)  = (p \cdot m) + (p \cdot n))$

\Prop 40.54 $(m,n,p, \in \nats \c (p \cdot m) + (p \cdot n) =  p \cdot (m + n))$

\Prop 40.55 $(0 < 1)$

\Prop 40.56 $(1 < 2)$

\Prop 40.57 $(2 < 3)$

\Prop 40.58 $(1 > 0)$

\Prop 40.59 $(2 > 1)$

\Prop 40.60 $(3 > 2)$

\Prop 40.61 $(A \i \nats \And A \ne \e \c \ex \Min A)$

\Prop 40.62 $(A \i \nats \And A \ne \e \And m \ident \Min A \c m = \Min A)$

\Prop 40.63 $(a,b,\in\nats \c a=b \Or a< b\Or a>b)$

\Prop 40.64 $(a,b,\in\nats \c  a\le  b\Or a\ge b)$

\Prop 40.65 $(a,b,\in\nats \c a \le b \Or b \le a)$

\Prop 40.66 $(a,b,\in\nats \c a \le b \Or a > b)$

\Prop 40.67 $(a,b,\in\nats \c a < b \Or  a \ge b)$

\Prop 40.68 $\Each a,b,\in\nats (a \le b \Or b \le a)$

\Prop 40.69 $(a \in \nats \c a \le a)$

\Prop 40.70 $(a,b,\in \nats \c a < b \Iff a+1 \le b)$

\Prop 40.71 $(a,b,\in \nats \c a > b \Iff a \ge b + 1)$

\Prop 40.72 $(a,b,\in \nats \c a < b \Iff a \le b -1)$

\Prop 40.73 $(a,b,\in \nats \c a > b \Iff a -1 \ge b )$

\Prop 40.74 $(a,b,\in\nats \c a \le a + b)$

\Prop 40.75 $(a,b,\in\nats \c a + b \ge a)$

\Prop 40.76 $(a,b,\in\nats \c b \le a + b)$

\Prop 40.77 $(a,b,\in\nats \c a + b \ge b)$

\Prop 40.78 $\Not \ex \Max \nats$

\Prop 40.79 $(0 = \Min \nats)$

\Prop 40.80 $(2 = 1 + 1)$

\Prop 40.81 $(3 = 2 + 1)$

\Prop 40.82 $(4 = 3 + 1)$


\lineb



\chap{41. Finite Cardinal Numbers}

%%%%primitive_term: \num A

%precedence= 6
\Prop 41.100 $((A \eq B) \Iff \Some f \.f : A \Iff B)$

\Prop 41.101 $(\num A \ident (A \in \fnt \cond \The x \in \nats(A \eq \.x\e)
\els \PI \setof x \in \Omega (A \eq x)))$

\prop 41.1 $(\ex\num A \c \ex A)$

\prop 41.2 $(\num A \in \nats \Iff A \in \fnt)$ 

\prop 41.3 $(\num A = 0 \Iff A = \e)$

\prop 41.4 $(\num A \ne 0 \c A \ne \e)$

\prop 41.5 $(\num A = 1 \Iff \Some x (A = \{x\}))$

\prop 41.6 $(\num A = 2 \Iff \Some x,y (x \ne  y \And A = \{x,y\}))$

\prop 41.7 $(\num A = 3 \Iff \Some x,y,z (x \ne  y \And x \ne  z \And y\ne z
\And A = \{x,y,z\}))$

\prop 41.8 $(A \cap B = \e \c \num (A \cup B) \ident \num A + \num B)$


\prop 41.9 $(\num A \in\nats \Iff  A \in \fnt)$

\Prop 41.10 $(\num A \in\ints \c \num A \in\nats)$

\Prop 41.11 $(A \in \fnt \And B \i A \c \num B \le \num A)$

\Prop 41.12 $(A \in \fnt \And \num B \le \num A \c B \in \fnt)$

\Prop 41.13 $(n \in \nats \And \num B \le n \c \num B \in \nats)$

\Prop 41.14 $(B \i A \And \num A \le n \c \num B \le n)$

\Prop 41.15 $(B \i A \And \num A \in \nats \c \num B \in \nats)$

\Prop 41.16 $(B \i A \And \num A = n \And n \in \nats\c \num B \le n)$

\Prop 41.17 $(\num A ,\num B ,\in \nats\And A \cap B = \e \c\num(A \cup B)=\num A+\num B)$

\Prop 41.18 $(\num (A \cup B)\in \nats\And A \cap B = \e \c\num(A \cup B)=\num A+\num B)$

\Prop 41.19 $\Not(\num\nats \in \nats)$

\Prop 41.20 $(\nats \notin \fnt)$

\Prop 41.21 $(\num A = 0 \Iff A = \e)$

\Prop 41.22 $(\num A > 0 \Iff A \ne \e \And A \in \fnt)$

\Prop 41.23 $(\num A = 1 \Iff \One x (x \in A))$

\Prop 41.24 $(\num A = 1 \Iff \Some x (A = \{x\}))$
\lineb

\chap{42. Very Small Sets}

\prop 42.1 $(x \in A \And \num A = 1 \c A = \{x\})$

\prop 42.2 $(\Not(\num A = 1) \Iff \ex A \And \Each x \in A \Some y \in A(y\ne x))$

\prop 42.3 $(\num A =  1 \And x,y, \in A \c x = y)$

\prop 42.4 $(x \in A \And \num A = 2 \c \One y\in A(y \ne x))$

\prop 42.5 $(x \in A \And \One y \in A(y \ne x) \c \num A = 2)$

\prop 42.6 $(\num A = 2 \And x,y,\ne,\in A \c A = \{x,y\})$

\prop 42.7 $(x,y,\ne,\in A \c \Not(\num A \le 1))$

\prop 42.8 $(\num A \le 2 \And x,y,\ne,\in A \c A = \{x,y\})$

\prop 42.9 $(x \ne y \And A = \{x,y\} \c \num A = 2)$

\Prop 42.10 $(\num A = 3 \And x,y,\ne,\in A \c
\One z \in A (x,y,\ne z))$

\Prop 42.11 $(x,y,z,\ne,\in A \c \Not(\num A \le 2))$

\Prop 42.12 $(\num A = 4 \And x,y,z,\ne,\in A \c
\One u \in A(x,y,z,\ne u))$

\Prop 42.13 $(\num A = 3 \And x,y,\ne,\in A \c \Some z(x,y,z,\ne,\in A))$

\Prop 42.14 $(\num A = 3 \And x \in A \c \Some y,z (x,y,z,\ne,\in A))$

\Prop 42.15 $(\num A = 3 \c \Some x,y,z (x,y,z,\ne,\in A))$

\Prop 42.16 $(\num A = 3 \And x,y,z,\ne,\in A \c A = \{x,y,z\})$

\Prop 42.17 $(x,y,z,\ne,\in A \And A \i \{x,y,z\}\c \num A = 3)$

\Prop 42.18 $(x,y,z,\ne,\in A \c \num A \ge 3)$

\Prop 42.19 $(x,y,z,\ne,\in A \And x,y,z,\in B
\c x,y,z,\ne,\in B)$
\lineb

\chap{43. Combinatorics}

%primitive_term: \sum x ; \pbar x \ubar x

\Prop 43.101 $(\odd \ident \setof n \in \nats\Some m \in \nats(n = 2 \cdot m + 1))$

\Prop 43.102 $(\even \ident \setof n \in \nats\Some m \in \nats(n = 2 \cdot m ))$

%precedence= 13
\Prop 43.103 $((a \Mod b) \ident (a,b,\in \ints \cond
\The x \in \nats \Some c \in \ints (a = b \cdot c + x)))$

\prop 43.1 $(A \in \fnt \And B \in \partition A \And \Each x \in B(\num x = n) 
\c \num A = n \cdot \num B)$

\prop 43.2 $(A \in \fnt \And B \in \partition A \c \num B \le  \num A)$

\prop 43.3 $(\bigcup x \in I \ubar x\in \fnt \And 
\setof \ubar x \ls x \in I \rs\in\disjoint 
\c \num \bigcup x \in I \ubar x = \sum x \in I \num \ubar x)$

\prop 43.4 $( I \in \fnt \And
\setof \ubar x \ls x \in I \rs\in\disjoint 
\c \num \bigcup x \in I \ubar x \ident \sum x \in I \num \ubar x)$

\prop 43.5 $( \Each x \in I (\ubar x \i \vbar x) \And
\setof \vbar x \ls x \in I \rs\in\disjoint 
\c \setof \ubar x \ls x \in I \rs\in\disjoint)$ 

\prop 43.6 $( I \in \fnt \And \Each x \in I (\ubar x \in \ints)
\c \sum x \in I \ubar x \in \odd \Iff \num\setof x \in I (\ubar x \in\odd)\in\odd)$
\lineb

\chap{44. Using Natural Numbers as Tuple Indices}
\lineb

\prop 44.1 $(p = (a,b) \c p \_ 0 = a)$

\prop 44.2 $(p = (a,b) \c p \_ 1 = b)$

\prop 44.3 $((a,b) = p \c p \_ 0 = a)$

\prop 44.4 $((a,b) = p \c p \_ 1 = b)$

\prop 44.5 $(\ex (p\_ n) \c \ex p)$
\lineb

\chap{45. The Indexed Symmetric Difference}

\noindent{Definition}

\prop 45.1 $(\Symdif x ;\pbar x \ubar x \ident \setof y (\setof x ;\pbar x (y \in \ubar x) \in \odd))$

\noindent{Theorems}

\prop 45.2 $(a,b,\in\fnt \c\num (a \symdif b) = \num a + \num b - 2\cdot\num(a\cap b))$

\prop 45.3 $(a,b,c,\in\fnt \c \num (a \symdif b \symdif c) = \num a + \num b  + \num c 
- 2\cdot\num(a\cap b) - 2\cdot\num(a\cap c)-2\cdot\num(b\cap c)+4\cdot\num(a\cap b\cap c))$

\prop 45.4 $({\cal F} \in \fnt \And \Each x \in {\cal F}(\num\ubar x \in \even)
\c \num \Symdif x \in {\cal F}\ubar x \in \even)$

\prop 45.5 $({\cal F} \in \fnt 
\c \Symdif x \in {\cal F}\ubar x \cap B \ident\Symdif x \in {\cal F}(\ubar x \cap B ))$

\lineb

\chap{46.  Utilities for Finite Sequences}
\lineb

\noindent {Definitions}

\prop 46.1 $(\Int n\ident (n\in\nats\cond\setof k\in\nats(k \le n)))$

\prop 46.2 $(\fsqnc \ident \setof f \in\function\Some n\in\nats
(\dmn f = \lbrack 0, (n-1)\rbrack \cap \nats ))$

\prop 46.3 $(\Fsqnc A \ident  \setof f \in\fsqnc (\rng f \i A))$

\prop 46.4 $(\ddmn f \ident (f\in\function \cond\setof k \in \dmn f (k+1 \in \dmn f)))$

\prop 46.5 $(\first f \ident \.f \Min \dmn f)$

\prop 46.6 $(\last f \ident \.f \Max \dmn f)$

\prop 46.7 $(\Rev f \ident ( f = \e \cond \e\els  
f\in\fsqnc\cond\Case m = \Max\dmn f \lonzo j \in \Int m\.f(m - j) ))$

\prop 46.8 $(\splice fg\ident (f,g,\in\fsqnc\And \.g0 = \last f\cond 
\Case m  = \Max \dmn f  \lonzo n(\.fn\els\.g(n-m))))$

\prop 46.9 $(\slice fmn \ident (f \in \fsqnc \And m,n,\le,\in\dmn f\cond \lonzo k \le n-m \.f(k+m)))$

\Prop 46.10 $(\concat fg\ident (f,g,\in\fsqnc \cond
\Case m = \Max \dmn f \lonzo n (\.fn \els \.g (n - m - 1))))$

\Prop 46.11 $(\Enum A \ident \setof f\Some n\in\nats
	\.f: \Int n \Iff A)$

\Prop 46.12 $(\Rot f i \ident(f\in\fsqnc\And i\in\nats\cond 
	\Case n(\dmn f =\Int n 
	\cond \lonzo j \in \Int n\.f((j + i) \Mod n))))$
\lineb

\chap{47. Intervals of Integers }

\prop 47.1 $(\ex \Int n \Iff n \in \nats)$

\prop 47.2 $(\Int n \i \nats \Iff  n \in \nats)$

\prop 47.3 $(\Int n \in \fnt \Iff n \in \nats)$

\prop 47.4 $(\Int n \in \fnt \Iff \ex\Int n )$

\prop 47.5 $(\Int n \in \U \Iff n \in \nats)$

\prop 47.6 $(\Max \Int n = n \Iff n \in \nats)$

\prop 47.7 $(\Some n(A  = \Int n)\c \ex \Max A)$

\prop 47.8 $(\Min \Int n = 0 \Iff n \in \nats)$

\prop 47.9 $(0\in \Int n \Iff n \in \nats)$

\Prop 47.10 $(\num\Int n = n + 1 \Iff \ex \Int n)$

\Prop 47.11 $(n \in \Int n \Iff  n \in \nats)$

\Prop 47.12 $\Not (\nats = \Int n)$

\Prop 47.13 $(\Int 0 = \{0\})$

\Prop 47.14 $(\Int 1 = \{0,1\})$

\Prop 47.15 $(y = \Int n \c n \in \nats)$

\Prop 47.16 $(y = \Int n \c 0 \in y)$

\Prop 47.17 $(y = \Int n \c n \in y)$

\Prop 47.18 $(y = \Int n \c x \in y \Iff x \in \nats \And x \le n)$

\Prop 47.19 $(y = \Int n \And x \in\nats \c x \in y \Iff  x \le n)$

\Prop 47.20 $(x \in \Int n \c x \in\nats \And  x \le n)$

\Prop 47.21 $(n\in\nats \c x \in \Int n \Iff x \in\nats \And  x \le n)$

\Prop 47.22 $(y = \Int n \c y \i\nats)$

\Prop 47.23 $(A \i\Int n \And A\ne \e\c \ex \Max A)$

\Prop 47.24 $(A \i \Int n \And y = \Max A \c y \le n)$

\Prop 47.25 $(n\in\nats \And y > n \c y \notin \Int n)$


\Prop 47.26 $(f \in \fsqnc \c \dmn f \i \nats)$

\Prop 47.27 $(f \in \fsqnc \And n \in \dmn f \c n \in \nats)$

\Prop 47.28 $(f \ident \e \c f \in \fsqnc)$

\Prop 47.29 $(f \ident \e \c \dmn f = \e)$ 

\Prop 47.30 $(f \ident \e \c \rng f = \e)$ 

\Prop 47.31 $(f \ident \{(0,x)\} \And x \in \U \c f \in \fsqnc)$

\Prop 47.32 $(f \ident \{(0,x)\} \And x \in \U \c \dmn f = \Int 0)$

\Prop 47.33 $(f \ident \{(0,x)\} \And x \in \U \c \rng f = \{x\})$

\Prop 47.34 $(f \ident \{(0,x)\} \And x \in \U \c \.f0 = x)$

\Prop 47.35 $(f \ident \{(0,x)\} \And x \in \U \c \ddmn f = \e)$

\Prop 47.36 $(f \ident \{(0,x),(1,y)\} \And x,y, \in \U \c f \in \fsqnc)$

\Prop 47.37 $(f \ident \{(0,x),(1,y)\} \And x,y, \in \U \c \dmn f = \Int 1)$

\Prop 47.38 $(f \ident \{(0,x),(1,y)\} \And x,y, \in \U \c \rng f = \{x,y\})$

\Prop 47.39 $(f \ident \{(0,x),(1,y)\} \And x,y, \in \U \c \.f0 = x)$

\Prop 47.40 $(f \ident \{(0,x),(1,y)\} \And x,y, \in \U \c \.f1 = y)$

\Prop 47.41 $(f \in \fsqnc \c n = \Max\dmn f \Iff \dmn f = \Int n)$

\Prop 47.42 $(f \in \fsqnc \And \dmn g = \dmn f \c g \in \fsqnc)$

\Prop 47.43 $(f \in \fsqnc \And 0 \in \dmn f \c \ex \Max \dmn f)$

\Prop 47.44 $(f \in \fsqnc \And n \in \dmn f \And \Not(n \in \ddmn f)\c n = \Max\dmn f)$

\Prop 47.45 $(f \in \fsqnc \And 0 \in \dmn f \c \Max \dmn f \in \dmn f)$

\Prop 47.46 $(f \in \fsqnc \And 0 \in \dmn f \c \ex \last f)$

\Prop 47.47 $(f \in \fsqnc \And m \in \dmn f \And n \in \nats \And n \le m \c n \in\dmn f)$

\Prop 47.48 $(f \in \fsqnc \And m \in \dmn f \And n \in \nats \And n < m \c n \in\dmn f)$

\Prop 47.49 $(f \in \fsqnc \And m \in \dmn f \And n \ident \Max\dmn f\c n-m \in\dmn f)$

\Prop 47.50 $(f \in \fsqnc \c
n \ident \Max\dmn f \And 0\in\dmn f\Iff \dmn f = \Int n)$

\Prop 47.51 $(f \in \fsqnc \And n = \Max \dmn f
\c m \in \dmn f \Iff m \in \nats \And m \le n)$

\Prop 47.52 $(f \in \fsqnc \And \dmn f\ne \e \c 0 = \Min\dmn f)$

\Prop 47.53 $(f\in\fsqnc \c
\dmn f = \Int n \Iff \last f = \.fn)$

\Prop 47.54 $(\Some n(\dmn f = \Int n ) \c f \in \fsqnc )$

\Prop 47.55 $(\Some n\in\nats(\dmn f = \Int n) \c f \in \fsqnc \And 0 \in \dmn f)$


\Prop 47.56 $(n \in \ddmn f \c n \in \dmn f \And  n + 1 \in \dmn f)$

\Prop 47.57 $( n \in \dmn f \And  n + 1 \in \dmn f \c n \in \ddmn f )$

\Prop 47.58 $(n \in \ddmn f \Iff n \in \dmn f \And  n + 1 \in \dmn f)$

\Prop 47.59 $(n \in \ddmn f \c n + 1 \in \dmn f)$

\Prop 47.60 $(n \in \ddmn f \c n \in \dmn f)$

\Prop 47.61 $(\dmn f = \Int(n+1) \And n \in \nats\c \ddmn f = \Int n)$

\Prop 47.62 $(\dmn f = \dmn g \c \ddmn f = \ddmn g)$

\Prop 47.63 $(f \in \fsqnc \And k \in \dmn f \c k \in \nats)$

\Prop 47.64 $(f\in \function \c \ex \ddmn f)$

\Prop 47.65 $(f \in \fsqnc \And k \in \dmn f \And k > 0 \c k-1 \in \dmn f)$

\Prop 47.66 $(f \in \fsqnc \And k \in \dmn f \And j \in \nats\And j<k \c j \in \dmn f)$

\Prop 47.67 $(f\in\fsqnc \c f\in\function)$

\Prop 47.68 $(f\in\Fsqnc A \And \rng f \i B \c f\in\Fsqnc B)$

\Prop 47.69 $(s \in \fsqnc  \And \dmn s \ne \e \c  \Rev s  \in \fsqnc 
\And\dmn\Rev s=\dmn s \And \rng \Rev s = \rng s \And\Rev\Rev s=s)$

\Prop 47.70 $(g \ident \Rev f \c \ex g \Iff f \in \fsqnc)$

\Prop 47.71 $(f \in \fsqnc \And g \ident \Rev f \c g \in \fsqnc)$

\Prop 47.72 $(f \in \fsqnc \And g \ident \Rev f \c \dmn g = \dmn f)$

\Prop 47.73 $(f \in \fsqnc \And g \ident \Rev f \c \rng g = \rng f)$

\Prop 47.74 $(f \in \fsqnc \And n \ident \Max \dmn f \And g\ident \Rev f \And k \in \dmn f 
\c \.gk = \.f(n-k))$

\Prop 47.75 $(f \in \fsqnc \And n \ident \Max \dmn f \And g\ident \Rev f \And k \in \dmn f 
\c \.fk = \.g(n-k))$

\Prop 47.76 $(f \in \fsqnc \And 0 \in \dmn f \And g \ident \Rev f
\c \.g0 = \last f )$

\Prop 47.77 $(f \in \fsqnc\And 0 \in \dmn f  \And g \ident \Rev f
\c \last g = \.f0)$

\Prop 47.78 $(f \in\fsqnc\And 0 \in \dmn f \And g \ident \Rev f
\c g\in \fsqnc\And 0 \in \dmn g )$


\Prop 47.79 $(\ex \slice fmn \Iff f \in \fsqnc \And m,n,\le,\in\dmn f)$

\Prop 47.80 $(g = \slice fmn \c g \in \fsqnc)$

\Prop 47.81 $(g = \slice fmn \c 0 \in \dmn g )$

\Prop 47.82 $(g \ident \slice fmn \And k \in \dmn g \c \.gk = \.f(m+k))$

\Prop 47.83 $(m,n,\le,\in\dmn f \And f \in \fsqnc \And g \ident \slice fmn
\c k \in \dmn g \Iff k \in \nats \And k \le n-m)$

\Prop 47.84 $(g = \slice fmn \c \rng g = \lostar f \setof k\in\nats(m\le k\le n))$

\Prop 47.85 $(g = \slice fmn \c \.g0 = \.fm)$

\Prop 47.86 $(g = \slice fmn \c \last g = \.fn)$

\Prop 47.87 $(g = \slice fmn \c \rng g \i \rng f)$

\Prop 47.88 $(g = \slice fmn \c \dmn g = \Int(n-m))$

\Prop 47.89 $(\ex \splice fg \Iff f,g,\in \fsqnc \And \last f = \.g0)$

\Prop 47.90 $(h = \splice fg \c h \in \fsqnc)$

\Prop 47.91 $(h = \splice fg \c 0 \in \dmn h )$

\Prop 47.92 $(h = \splice fg \c \rng h = \rng f \cup \rng g)$

\Prop 47.93 $(h = \splice fg \c \.h0 = \.f0)$

\Prop 47.94 $(h = \splice fg \c \last h = \last g)$

\Prop 47.95 $(h = \splice fg \And \dmn f = \Int m \And \dmn g = \Int n
\c \dmn h = \Int (m+n))$

\Prop 47.96 $(h = \splice fg \And k \in \dmn f \c \.hk = \.fk)$

\Prop 47.97 $(h = \splice fg \And  k \in \dmn h \setdif \dmn f \And n \ident \Max\dmn f
\c \.hk = \.g(k - n))$

\Prop 47.98 $(h = \splice fg \And  n \ident \Max \dmn f \And k \in \nats \And k \ge n
\c \.hk \ident \.g(k - n))$

\Prop 47.99 $(h = \splice fg \And  n \ident \Max \dmn f \And k \in \dmn h \And k \ge n
\c \.hk = \.g(k - n))$


\Prop 47.100 $(s \in \fsqnc \And i \in \nats \And \dmn s =\Int n$
\lineb$ \c  \Rot s i \in \fsqnc \And\dmn\Rot si=\dmn s
\And\rng \Rot s i = \rng s \And$
\lineb$ (i \Mod n = 0 \c \Rot si = s))$

\Prop 47.101 $(s \in \fsqnc 
\And i,j, \in \nats \And \dmn s = \Int n \c$  
\lineb$ \Rot \Rot s i j = \Rot s (i + j) \And$
\lineb$ ((i + j) \Mod n = 0 \c \Rev \Rot s i = \Rot \Rev s j))$
\lineb



\noindent{Infinite sequences}

\Prop 47.103 $(\sqnc \ident\setof f (\dmn f = \nats))$ 

\Prop 47.102 $(\Sqnc A \ident (\ex A \cond \setof f \in\sqnc (\rng f \i A)))$
\lineb


\chap{48. Recursive Functions}

\prop 48.1 $(\clonzo f,n \ubarp fn \ident \Closure f 
	(\{(0,\Case n = 0 \ubarp fn)\} \cup
	f \cup \Case n = \Max \dmn f \{(n+1 , \ubarp fn)\}))$

\prop 48.2 $(\Fibonacci \ident \clonzo f,n
	(n \in \{0,1\}\cond 1\els\.f(n-1)+\.f(n-2)))$
\lineb

\chap{49. Ordinary Induction}
\lineb


\prop 49.1 $(0\in M \And \Each n\in M ( n+1\in M)\c \nats\i M)$

\prop 49.2 $(m \in \nats \And M = \setof n\in\nats \pbar n
	\And 0 \in M \And \Each n \in \nats 
	(n\in M \c n+1\in M) \c \pbar m)$

\prop 49.3 $(f\in \fsqnc \And 0 \in M \And
\Each n \in \ddmn f (n  \in M \c n + 1 \in M)\c \dmn f\i M)$

\prop 49.4 $(n \in \nats \And 0 \in M \And 
\Each k (k \in M \And k < n \c k + 1 \in M)\c \Int n\i M)$
\lineb


 
\chap{50. Sequences Defined by Induction}
\lineb

\noindent {Definitions}

\prop 50.1 $(\indc\pp Ta \ident \clonzo F,n (n=0 \cond a \els \.T(n,\.Fn)))$

\prop 50.2 $(\indc\p Ta \ident \indc\pp \lonzo n,x \.Tx a)$
\lineb

\noindent {Theorems}

\prop 50.3 $(\indc\pp Ta \ident \The f \in\function(\dmn f \i
	\nats  \And $
	$\.f0 = a \And \Each k \in \nats
	(\.f(k+1) \ident \.T(k,\.fk))))$

\prop 50.4 $(F \ident \indc\p Tx \c \ex F \Iff x \in \U)$

\prop 50.5 $(F \ident \indc\p Tx \c x \in \U \Iff \functionp F)$

\prop 50.6 $(F \ident \indc\p Tx \And (\ex x \c x \in \U) 
		\c \.F0 \ident x)$

\prop 50.7 $(F \ident \indc\p Tx \c x \in \U \Iff \.F0 = x)$

\prop 50.8 $(F \ident \indc\p Tx \c x \in \U \Iff \dmn F \i \nats)$

\prop 50.9 $(F \ident \indc\p Tx \c \ex F \Iff F \in \U)$

\Prop 50.10 $(F \ident \indc\p Tx \And n \in \nats \c
	\.F(n+1) \ident \.T\.Fn)$

\Prop 50.11 $(F = \indc\p Tx \c \rng F \i \rng T \cup \{x\})$

\Prop 50.12 $(F = \indc\p Tx \c \dmn F = \nats \Or \Some n \in \nats(\dmn F=\Int n))$

\Prop 50.13 $(F = \indc\p Tx \And n \in \dmn F\And m \in \nats \And m \le n\c m\in\dmn F)$

\Prop 50.14 $(F = \indc\p Tx \And n \in \dmn F \And \Not(n+1\in\dmn F)\c \dmn F=\Int n)$

\Prop 50.15 $(F = \indc\p Tx \c \dmn F \i \nats)$

\Prop 50.16 $(F = \indc\p Tx \c \.F0 = x)$

\Prop 50.17 $(F \ident (\pvar \cond \indc\p Tx) \c
\ex F \Iff \pvar \And x \in \U)$

\Prop 50.18 $(F = \indc\p Tx \And \.Fm = y \And G \ident \indc\p Ty$
\lineb$ \c \ex G \And \dmn G = \setof k \in \nats(m+k\in\dmn F)\And
\Each k \in \dmn G(\.Gk=\.F(m+k)))$

\Prop 50.19 $(F \ident (\pvar \cond \indc\p Tx)
\And (\pvar \c x \in \U) \c \ex F \Iff \pvar )$

\Prop 50.20 $(\ex\indc\p Tx \c \indc\p Tx\in\U \And x \in \U)$

\Prop 50.21 $\Each x(\ex\indc\p Tx \c \indc\p Tx\in\U \And x \in \U)$

\Prop 50.22 $\Not\ex\indc\p T\Nul$

\Prop 50.23 $(F\ident\lonzo z \indc\p Tz \c \.Fy \ident \indc\p Ty)$ 

\Prop 50.24 $(F  \ident \lonzo z \indc\p Tz\c \ex\.FZ\Iff Z \in \U)$

\Prop 50.25 $(F  \ident \lonzo z \indc\p Tz\c Z\in\U \Iff \functionp \.FZ)$

\Prop 50.26 $( F \ident \lonzo z \indc\p Tz \c Z\in\U
\Iff \.\.F Z 0  = Z)$

\Prop 50.27 $(
	F  \ident \lonzo z \indc\p Tz\And
\ex\.FZ\c \dmn \.FZ\i\nats)$


\Prop 50.28 $(F \ident \lonzo z \indc\p Tz 
	\And  n \in \nats 
	\c \.\.FZ(n+1) \ident \.T\.\.FZn)$

\Prop 50.29 $(F \ident \lonzo z \indc\p Tz 
	\And n,m, \in \nats 
	\c \.\.FZ(n+m) \ident \.\.F\.\.FZnm)$

\Prop 50.30 $(F \ident \lonzo z \indc\p Tz 
	\And n \in \nats 
	\c n+1\in\dmn \.FZ\Iff n\in\dmn \.FZ
\And \ex \.T\.\.FZn)$

\Prop 50.31 $(\functionp T \And 	F \ident \lonzo z \indc\p Tz
\And Z \in \dmn T \And \rng T \i \dmn T 
\c \ex \.\.FZn \Iff n \in \nats)$

\Prop 50.32 $(
	F  = \lonzo z \indc\p Tz\And Z\in\U
	\c \dmn \.FZ = \nats \Or \Some n\in\nats(\dmn \.FZ = \Int(n+1)))$

\Prop 50.33 $(F = \indc\p Tx \c \dmn F = \nats \Or
\Some n \in \nats (\dmn F = \Int(n+1)))$ 
\lineb

\chap{51. Periodic functions}
\lineb

\noindent {Definitions}

\prop 51.1 $(\repeaters f \ident \setof y > 0
 \Each z \in \dmn f(\.f(z + y)=\.fz))$

\prop 51.2 $(\period f \ident \Min \repeaters f )$

\Prop 51.15 $(\divisor n \ident (n \in \ints \cond \setof m \in \ints\Some p(n=m\cdot m)))$
\lineb

\noindent{}Note that because we do not want to restrict the use of
the form `$\period f$' to integers we consider all 
{\it positive} $y$ in the definition of $\repeaters f$.
51.5 then relies on 50.26 and the fact that there is no smallest
positive number.

\noindent {Theorems}

\prop 51.3 $(x = \period f \c x > 0 \And 
 \Each z \in \dmn f(\.f(z + x)=\.fz))$

\prop 51.4 $(\dmn f = \e \c \repeaters f = \setof y (y > 0))$

\prop 51.5 $(x = \period f \c \dmn f \ne \e)$

\prop 51.6 $(	F  =  \indc\p TZ \And n > 0 \And \.Fn=\.F0 \c  \ex \period F )$

\prop 51.7 $(	F  = \indc\p TZ
\And \ex\period F
	\c \dmn F = \nats )$

\prop 51.8 $(	F  =  \indc\p TZ \And T \in \onetoone
\And \dmn F = \nats
\And \rng F \in \fnt \c \ex\period F)$ 
 
\prop 51.9 $(	F  =  \indc\p TZ \And T \in \onetoone
\And m < n \And \.Fm = \.Fn \c \period F \in \divisor (n-m))$ 
 
\Prop 51.10 $(F  = \indc\p TZ\And k = \period F 
		\And \.Fm = \.Fn \And m<n $
	$ \c \Some j \in \nats (j \cdot k = n - m))$

\Prop 51.11 $(F  = \indc\p TZ\And k = \period F $
	$ \c k \in \nats)$

\Prop 51.12 $(F  = \indc\p TZ\And k = \period F $
	$ \c k > 0)$

\Prop 51.13 $(k = \period f \And \dmn f = \nats \c \Each x \in \nats
(\.f(x+k)=\.fx))$

\Prop 51.14 $(k = \period f \And \dmn f = \nats \And x \in \nats \c
(\.f(x+k)=\.fx))$
\lineb



\lineb

\chap{52. Integers}

\prop 52.8 $(\even \ident \setof (2 \cdot x)\ls x \in \ints \rs)$

\Prop 52.11 $(\odd \ident (\ints \setdif \even))$

\prop 52.1 $\ex\ints$

\prop 52.2 $(\nats \i \ints)$

\prop 52.3 $(n \in \nats \c n \in \ints)$

\prop 52.4 $(m,n, \in \ints \c m-n \in \ints)$

\prop 52.5 $(m,n, \in \ints \c m+n \in \ints)$

\prop 52.6 $(m \in \ints \c (- m) \in \ints)$

\prop 52.7 $(n \in \ints \And m+ n \in \ints \c m \in \ints)$

\prop 52.9 $(n \in \ints \c 2\cdot n \in \even)$

\Prop 52.10 $(n \in \nats \c 2\cdot n \in \even)$

\Prop 52.12 $(\setof x\pbar x\in\fnt 
\c \Symdif x;\pbar x\setof y\qbarp xy =\setof y(\num \setof x ;\pbar x \qbarp xy \in \odd))$

\Prop 52.13 $(\setof x\pbar x\in\fnt \And \Each x ;\pbar x \ex\ubar x 
\c \setof y (\num \setof x ;\pbar x(y \in \ubar x) \in \odd)= \Symdif x ;\pbar x\ubar x )$

\Prop 52.14 $(\Each x;\pbar x(\ubar x \ident \vbar x) \c \Symdif x;\pbar x\ubar x\ident\Symdif x;\pbar x\vbar x)$

\Prop 52.15 $(\Each x;\pbar x(\vbar x \ident \ubar x) \c \Symdif x;\pbar x\ubar x\ident\Symdif x;\pbar x\vbar x)$

\Prop 52.16 $((0-1)  = (-1))$

\Prop 52.17 $(n \in \nats \c (n-1) + 1 = n)$

\Prop 52.18 $(n \in \nats \c n-1 < n)$

\Prop 52.19 $(n \in \nats \c n-1 \le n)$

\Prop 52.20 $(n \in \ints \c n-1 < n)$

\Prop 52.21 $(n \in \ints \c n-1 \le n)$

\Prop 52.22 $(n \in \nats \c n+1 > n)$

\Prop 52.23 $(n \in \nats \c n+1 \ge n)$

\Prop 52.24 $(n \in \ints \c n+1 > n)$

\Prop 52.25 $(n \in \ints \c n+1 \ge n)$

\Prop 52.26 $(n \in \ints \And m \in \nats \c n \le n+m)$

\Prop 52.27 $(n \in \ints \And m \in \nats \c n+m \ge n)$

\Prop 52.28 $(m\in \ints \And n\in \ints \And m+1=n+1\c m = n)$

\Prop 52.29 $(n\in \ints \And m+1=n+1\c m = n)$

\Prop 52.30 $(m\in \ints \And m+1=n+1\c m = n)$

\Prop 52.31 $(n\in \nats \And m+1=n+1\c m = n)$

\Prop 52.32 $(m\in \nats \And m+1=n+1\c m = n)$

\Prop 52.33 $(m\in \ints \And n\in \ints \And 1+m=1+n\c m = n)$

\Prop 52.34 $(n\in \ints \And 1+m=1+n\c m = n)$

\Prop 52.35 $(m\in \ints \And 1+m=1+n\c m = n)$

\Prop 52.36 $(n\in \nats \And 1+m=1+n\c m = n)$

\Prop 52.37 $(m\in \nats \And 1+m=1+n\c m = n)$

\Prop 52.38 $(n \in \ints \c (n+1) -1 = n)$

\Prop 52.39 $(-1 \in \U)$

\Prop 52.40 $\ex (-1)$ 

\Prop 52.41 $(1 \in \ints)$

\Prop 52.42 $(1 \in \odd)$

\Prop 52.43 $(0 \in \ints)$

\Prop 52.44 $(0 \in \even)$

\Prop 52.45 $(2 \in \ints)$

\Prop 52.46 $(2 \in \even)$

\Prop 52.47 $(x \in \even \c x \notin \odd)$

\Prop 52.48 $(x \in \odd \c x \notin \even)$

\Prop 52.49 $(x \in \even \c \Not(x \in \odd))$

\Prop 52.50 $(x \in \odd \c \Not(x \in \even))$

\Prop 52.51 $(x \in \even \And y \in \even \c x + y \in \even)$

\Prop 52.52 $(x \in \odd \And y \in \odd \c x + y \in \even)$

\Prop 52.53 $(x \in \even \And y \in \even \c x - y \in \even)$

\Prop 52.54 $(x \in \odd \And y \in \odd \c x - y \in \even)$

\Prop 52.55 $(x \in \ints \Iff x \in \even \Or x \in \odd)$

\Prop 52.56 $(x \in \nats \c x \in \even \Or x \in \odd)$

\Prop 52.57 $(n \in \nats \c (- n) +  n = 0)$

\Prop 52.58 $(n \in \ints \c n + 0 = n)$

\Prop 52.59 $(n \in \ints \c 0 + n = n)$

\Prop 52.60 $(1 - 1 = 0)$

\Prop 52.61 $(n\in\ints \c n - n = 0)$

\Prop 52.62 $(n\in\nats \c n - n = 0)$

\Prop 52.63 $(n \in \nats \And m + n = 0 \c m = (-n))$

\Prop 52.64 $(m,n,\in \nats \c (n - m) + m = n)$

\Prop 52.65 $(m,n,\in \ints \c (n - m) + m = n)$

\Prop 52.66 $(m,n,\in \ints \c n = (n + m)  - m )$

\Prop 52.67 $(m,n,\in \nats \c n = m + (n - m) )$

\Prop 52.68 $(m,n,\in \ints \c n = m + (n - m) )$

\Prop 52.69 $(m,n,\in \ints \c  (n + m)  - m = n)$

\Prop 52.70 $(m,n,\in \nats \c  (n + m)  - m = n)$

\Prop 52.71 $(m,n,\in \nats \c  m + (n - m) = n)$

\Prop 52.72 $(m,n,\in \ints \c m + (n - m) = n )$

\Prop 52.73 $(m,n,\in \nats \c m + (n - m) = n )$

\Prop 52.74 $(a,b,c, \in \ints \c (a + c) + b = (a + b) + c)$

\Prop 52.75 $(a,b,c, \in \nats \c (a + c) + b = (a + b) + c)$

\Prop 52.76 $(a,b,c, \in\ints \c (a - b) + c = a - (b - c))$

\Prop 52.77 $(a,b,c, \in\nats \c (a - b) + c = a - (b - c))$

\Prop 52.78 $(a,b,c, \in\ints \c (a - b) - c = a - (b + c))$

\Prop 52.79 $(a,b,c, \in\nats \c (a - b) - c = a - (b + c))$

\Prop 52.80 $(a,b,c, \in\ints \c a - (b + c) = (a - b) - c )$

\Prop 52.81 $(a,b,c, \in\nats \c a - (b + c) = (a - b) - c )$

\Prop 52.82 $(a,b,c, \in\ints \c (a - c) + b = (a + b) - c )$

\Prop 52.83 $(a,b,c, \in\nats \c (a - c) + b = (a + b) - c )$

\Prop 52.84 $(m,n,\in \nats \c m - n \in \nats
\Iff n \le m)$

\Prop 52.85 $(m,n,\in \ints \c m - n \in \nats
\Iff n \le m)$

\Prop 52.86 $(m,n, \in \nats \c m < n \Iff
m + 1 \le n)$

\Prop 52.87 $(m,n,\in\nats \And m < n \c n - m \in \nats)$

\Prop 52.88 $(m,n,\in\nats \And m < n \c (n - m) - 1 \in \nats)$

\Prop 52.89 $(m,n, \in \ints \c m < n \Iff
m + 1 \le n)$

\Prop 52.90 $(a,b,c, \in \nats \And a < b
\c a + c < b + c)$

\Prop 52.91 $(a,b,c, \in \nats \And a < b
\c  c + a < c +  b )$

\Prop 52.92 $(a,b,c, \in \ints \And a < b
\c a + c < b + c)$

\Prop 52.93 $(a,b, \in \nats \c a \le a + b)$

\Prop 52.94 $(a,b, \in \nats \c b \le a + b)$

\Prop 52.95 $(a,b,\in \nats \c a - b \le a )$

\Prop 52.96$(a,b,c, \in \ints \And a < b
\c a - c < b - c)$

\Prop 52.97 $(a,b,c, \in \ints \And a < b
\c  c + a < c +  b )$

\Prop 52.98$(a,b,c, \in \nats \And a < b
\c a - c < b - c)$

\Prop 52.99 $(m,n, \in \ints \c m > n \Iff
m + 1 \ge n)$

\Prop 52.100 $(a,b,c, \in \nats \And a > b
\c a + c > b + c)$

\Prop 52.101 $(a,b,c, \in \nats \And a > b
\c c + a  > c + b )$

\Prop 52.102 $(a,b,\in \nats \c a > b \Iff a - b > 0)$

\Prop 52.103 $(a,b, \in \ints \c a < b \Iff b > a)$

\Prop 52.104 $(a,b,\in \ints \And a \ne b\c a < b\Or a > b)$

\Prop 52.105 $(m \in \nats \And n - m \in \nats \c n \in \nats)$

\Prop 52.106 $(n \in \nats \And m - n = -n \c m = 0)$ 

\Prop 52.107 $(n \in \nats \And m + n = n \c m =  0)$

\Prop 52.108 $(m \in \ints \And m + n = m \c n = 0)$

\Prop 52.109 $(m \in \ints \c m + 1 \ne m)$

\Prop 52.110 $(A \i \nats \And A \ne \e \c \ex \Min A)$

\Prop 52.111 $(m \in \ints \Iff (-m) \in \ints)$

\Prop 52.112 $(m,n, \in \ints \c m - n = m + (-n))$

\lineb  

\chap{53. Rational Numbers}

%primitive_term: \rats

\prop 53.1 $(x,y, \in \rats \c x + y \in \rats)$

\lineb  

\chap{54. Real Numbers}

%primitive_term: \reals

\prop 54.1 $(x,y, \in \reals \c x + y \in \reals)$

\prop 54.2 $(x,y, \in \reals \c x \cdot y \in \reals)$

\prop 54.3 $(\ints \i \reals)$

\prop 54.4 $(0 \in \reals)$

\prop 54.5 $(1 \in \reals)$ 

\prop 54.6 $((-1) \in \reals)$

\prop 54.7 $(x \in \reals \c x + 0 = x)$

\prop 54.8 $(x \in \reals \c x = x + 0)$

\prop 54.9 $(x \in \reals \c x - x = 0)$

\Prop 54.10 $(x \in \reals \c 0 = x - x)$

\Prop 54.11 $(x,y, \in \reals \c  x - y =  (- (y - x)))$

\Prop 54.12 $(x,y,z, \in \reals \c x \cdot (y + z) = x \cdot y +  x \cdot z)$
\lineb



\chap{13. Group Theory}
\lineb

\noindent{Definitions}

\Prop 24.102 $(\permute A \ident (A \in \U \cond \setof p \. p:A \Iff A))$

\Prop 54.13 $(\newspace Xf \ident \setof (\{(\e, x)\} \cup f) \ls x \in X \rs)$

\Prop 54.14 $(\group \ident \setof G \in\Space\Some e \in G \Each x,y, \in G \Some z \in G
	(x \cdot y \in G \And e \cdot x = x \And z \cdot x = e))$

\Prop 54.15 $(\ulone G \ident \The e \in G \Each x \in G
	(e \cdot x = x))$

\Prop 54.16 $(\lab X \rab \ident (\Some G \in \group(\e \ne X \i G) \cond
	\bigcap G \in \group:(X \i G)))$

\Prop 54.17 $(\symgset X \ident (X \in U \cond \Case f = \lonzo p,x \in
	 \permute X \lilx X \.px \newspace X \{(\ultimes, f)\}))$

\Prop 54.18 $(\Sym A \ident (A \in \U \cond \Case f = \lonzo x,y, \in 
	\permute A (y \cmp x) \newspace A \{(\ultimes, f)\}))$

\Prop 54.19 $(\symorbit XGa \ident (a \in X \And G \i \Sym X \cond
	\setof y \in \symgset X \Some z \in G (y = z \cdot x)))$

\Prop 54.20 $(\transgp X \ident (X \in \U \cond \setof G \in \group 
	\Each x \in \symgset X(\symgset X = \symorbit XGx)))$
\lineb




\end
