This theory file deals with results on cardinal numbers (cardinals). Cardinals are a genaralization of the natural numbers, used to measure the cardinality (size) of sets. Contributed by Daniel de la Concepcion.

All the results of this section are done without assuming the Axiom of Choice. With the Axiom of Choice in play, the proofs become easier and some of the assumptions may be dropped.

Since General Topology Theory is closely related to Set Theory, it is very interesting to make use of all the possibilities of Set Theory to try to classify homeomorphic topological spaces. These ideas are generally used to prove that two topological spaces are not homeomorphic.

There exist cardinals which are the successor of another cardinal, but as happens with ordinals, there are cardinals which are limit cardinal.

** Definition **

\( \text{LimitC}(i) \equiv \text{Card}(i) \wedge 0 \lt i \wedge (\forall y.\ (y \lt i\wedge \text{Card}(y)) \longrightarrow \text{csucc}(y) \lt i) \)

Simple fact used a couple of times in proofs.

** lemma ** nat_less_infty:

** assumes **\( n\in nat \)** and **\( \text{InfCard}(X) \)

There are three types of cardinals, the zero one, the succesors of other cardinals and the limit cardinals.

** lemma ** Card_cases_disj:

** assumes **\( \text{Card}(i) \)

Given an ordinal bounded by a cardinal in ordinal order, we can change to the order of sets.

** lemma ** le_imp_lesspoll:

** assumes **\( \text{Card}(Q) \)

There are two types of infinite cardinals, the natural numbers and those that have at least one infinite strictly smaller cardinal.

** lemma ** InfCard_cases_disj:

** assumes **\( \text{InfCard}(Q) \)

{
** assume **\( \forall j.\ \neg \text{csucc}(j) \preceq Q \vee \neg \text{InfCard}(j) \)
** then **** have ** D: \( \neg \text{csucc}(nat) \preceq Q \)** using ** InfCard_nat
** with **D, assms ** have ** \( \neg (\text{csucc}(nat) \leq Q) \)** using ** le_imp_lesspoll , InfCard_is_Card
** with **assms ** have ** \( Q \lt (\text{csucc}(nat)) \)** using ** not_le_iff_lt , Card_is_Ord , Card_csucc , Card_is_Ord , Card_is_Ord , InfCard_is_Card , Card_nat
** with **assms ** have ** \( Q\leq nat \)** using ** Card_lt_csucc_iff , InfCard_is_Card , Card_nat
** with **assms ** have ** \( Q=nat \)** using ** InfCard_def , le_anti_sym
** } **
** thus ** \( thesis \)
** qed **

A more readable version of standard Isabelle/ZF *Ord_linear_lt*

** lemma ** Ord_linear_lt_IML:

** assumes **\( Ord(i) \), \( Ord(j) \)

A set is injective and not bijective to the successor of a cardinal if and only if it is injective and possibly bijective to the cardinal.

** lemma ** Card_less_csucc_eq_le:

** assumes **\( \text{Card}(m) \)

If the successor of a cardinal is infinite, so is the original cardinal.

** lemma ** csucc_inf_imp_inf:

** assumes **\( \text{Card}(j) \)** and **\( \text{InfCard}(\text{csucc}(j)) \)

{
** assume **f: \( Finite (j) \)
** then **** obtain **\( n \)** where **\( n\in nat \), \( j\approx n \)** using ** Finite_def
** with **assms(1) ** have ** TT: \( j=n \), \( n\in nat \)** using ** cardinal_cong , nat_into_Card , Card_def
** then **** have ** Q: \( succ(j)\in nat \)** using ** nat_succI
** with **f, TT ** have ** T: \( Finite(succ(j)) \), \( \text{Card}(succ(j)) \)** using ** nat_into_Card , nat_succI
** from **T(2) ** have ** \( \text{Card}(succ(j))\wedge j \lt succ(j) \)** using ** Card_is_Ord
** moreover ** ** from **this ** have ** \( Ord(succ(j)) \)** using ** Card_is_Ord
** moreover ** {
** fix **\( x \)
** assume **A: \( x \lt succ(j) \)
{
** assume **\( \text{Card}(x)\wedge j \lt x \)
** with **A ** have ** \( False \)** using ** lt_trans1
** } **
** hence ** \( ~(\text{Card}(x)\wedge j \lt x) \)
** } **
** ultimately **** have ** \( (\ \lt mu> L.\ \text{Card}(L) \wedge j \lt L)=succ(j) \)** by (rule **Least_equality** ) **
** then **** have ** \( \text{csucc}(j)=succ(j) \)** using ** csucc_def
** with **Q ** have ** \( \text{csucc}(j)\in nat \)
** then **** have ** \( \text{csucc}(j) \lt nat \)** using ** lt_def , Card_nat , Card_is_Ord
** with **assms(2) ** have ** \( False \)** using ** InfCard_def , lt_trans2
** } **
** then **** have ** \( ~(Finite (j)) \)
** with **assms(1) ** show ** \( thesis \)** using ** Inf_Card_is_InfCard
** qed **

Since all the cardinals previous to *nat*
are finite, it cannot be a successor cardinal hence it is
a *LimitC* cardinal.

** corollary ** LimitC_nat:

If two sets are strictly injective to an infinite cardinal,
then so is its union. For the case of successor cardinal, this
theorem is done in the isabelle library in a more general setting
but that theorem is of not
use in the case where \( \text{LimitC}(Q) \) and it also makes use
of the Axiom of Choice. The mentioned theorem is in the
theory file *Cardinal_AC.thy*

Note that if \(Q\) is finite and different from \(1\), let's assume \(Q=n\), then the union of \(A\) and \(B\) is not bounded by \(Q\). Counterexample: two disjoint sets of \(n-1\) elements each have a union of \(2n-2\) elements which are more than \(n\).

Note also that if \(Q=1\) then \(A\) and \(B\) must be empty
and the union is then empty too and \(Q\) cannot be *0* because
no set is injective and not bijective to *0*.

The proof is divided in two parts, first the case when both sets \(A\) and \(B\) are finite and second, the part when at least one of them is infinite. In the first part, it is used the fact that a finite union of finite sets is finite. In the second part it is used the linear order on cardinals (ordinals). This proof can not be generalized to a setting with an infinite union easily.

** lemma ** less_less_imp_un_less:

** assumes **\( A\prec Q \)** and **\( B\prec Q \)** and **\( \text{InfCard}(Q) \)

{
** assume **\( Finite (A) \wedge Finite(B) \)
** then **** have ** \( Finite(A \cup B) \)** using ** Finite_Un
** then **** obtain **\( n \)** where **R: \( A \cup B \approx n \), \( n\in nat \)** using ** Finite_def
** then **** have ** \( |A \cup B| \lt nat \)** using ** lt_def , cardinal_cong , nat_into_Card , Card_def , Card_nat , Card_is_Ord
** with **assms(3) ** have ** T: \( |A \cup B| \lt Q \)** using ** InfCard_def , lt_trans2
** from **R ** have ** \( Ord(n) \), \( A \cup B \preceq n \)** using ** nat_into_Card , Card_is_Ord , eqpoll_imp_lepoll
** then **** have ** \( A \cup B\approx |A \cup B| \)** using ** lepoll_Ord_imp_eqpoll , eqpoll_sym
** also ** ** from **T, assms(3) ** have ** \( \ldots \prec Q \)** using ** lt_Card_imp_lesspoll , InfCard_is_Card
** finally **** have ** \( A \cup B\prec Q \)
** } **
** moreover ** {
** assume **\( ~(Finite (A) \wedge Finite(B)) \)
** hence ** A: \( ~Finite (A) \vee ~Finite(B) \)
** from **assms ** have ** B: \( |A|\approx A \), \( |B|\approx B \)** using ** lesspoll_imp_eqpoll , lesspoll_imp_eqpoll , InfCard_is_Card , Card_is_Ord
** from **B(1) ** have ** Aeq: \( \forall x.\ (|A|\approx x) \longrightarrow (A\approx x) \)** using ** eqpoll_sym , eqpoll_trans
** from **B(2) ** have ** Beq: \( \forall x.\ (|B|\approx x) \longrightarrow (B\approx x) \)** using ** eqpoll_sym , eqpoll_trans
** with **A, Aeq ** have ** \( ~Finite(|A|)\vee ~Finite(|B|) \)** using ** Finite_def
** then **** have ** D: \( \text{InfCard}(|A|)\vee \text{InfCard}(|B|) \)** using ** Inf_Card_is_InfCard , Inf_Card_is_InfCard , Card_cardinal
{
** assume **AS: \( |A| \lt |B| \)
{
** assume **\( ~\text{InfCard}(|A|) \)
** with **D ** have ** \( \text{InfCard}(|B|) \)
** } **
** moreover ** {
** assume **\( \text{InfCard}(|A|) \)
** then **** have ** \( nat\leq |A| \)** using ** InfCard_def
** with **AS ** have ** \( nat \lt |B| \)** using ** lt_trans1
** then **** have ** \( nat\leq |B| \)** using ** leI
** then **** have ** \( \text{InfCard}(|B|) \)** using ** InfCard_def , Card_cardinal
** } **
** ultimately **** have ** INFB: \( \text{InfCard}(|B|) \)
** then **** have ** \( 2 \lt |B| \)** using ** nat_less_infty
** then **** have ** AG: \( 2\preceq |B| \)** using ** lt_Card_imp_lesspoll , Card_cardinal , lesspoll_def
** from **B(2) ** have ** \( |B|\approx B \)
** also ** ** from **assms(2) ** have ** \( \ldots \prec Q \)
** finally **** have ** TTT: \( |B|\prec Q \)
** from **B(1) ** have ** \( \text{Card}(|B|) \), \( A \preceq |A| \)** using ** eqpoll_sym , Card_cardinal , eqpoll_imp_lepoll
** with **AS ** have ** \( A\prec |B| \)** using ** lt_Card_imp_lesspoll , lesspoll_trans1
** then **** have ** I1: \( A\preceq |B| \)** using ** lesspoll_def
** from **B(2) ** have ** I2: \( B\preceq |B| \)** using ** eqpoll_sym , eqpoll_imp_lepoll
** have ** \( A \cup B\preceq A+B \)** using ** Un_lepoll_sum
** also ** ** from **I1, I2 ** have ** \( \ldots \preceq |B| + |B| \)** using ** sum_lepoll_mono
** also ** ** from **AG ** have ** \( \ldots \preceq |B| * |B| \)** using ** sum_lepoll_prod
** also ** ** from **assms(3), INFB ** have ** \( \ldots \approx |B| \)** using ** InfCard_square_eqpoll
** finally **** have ** \( A \cup B\preceq |B| \)
** also ** ** from **TTT ** have ** \( \ldots \prec Q \)
** finally **** have ** \( A \cup B\prec Q \)
** } **
** moreover ** {
** assume **AS: \( |B| \lt |A| \)
{
** assume **\( ~\text{InfCard}(|B|) \)
** with **D ** have ** \( \text{InfCard}(|A|) \)
** } **
** moreover ** {
** assume **\( \text{InfCard}(|B|) \)
** then **** have ** \( nat\leq |B| \)** using ** InfCard_def
** with **AS ** have ** \( nat \lt |A| \)** using ** lt_trans1
** then **** have ** \( nat\leq |A| \)** using ** leI
** then **** have ** \( \text{InfCard}(|A|) \)** using ** InfCard_def , Card_cardinal
** } **
** ultimately **** have ** INFB: \( \text{InfCard}(|A|) \)
** then **** have ** \( 2 \lt |A| \)** using ** nat_less_infty
** then **** have ** AG: \( 2\preceq |A| \)** using ** lt_Card_imp_lesspoll , Card_cardinal , lesspoll_def
** from **B(1) ** have ** \( |A|\approx A \)
** also ** ** from **assms(1) ** have ** \( \ldots \prec Q \)
** finally **** have ** TTT: \( |A|\prec Q \)
** from **B(2) ** have ** \( \text{Card}(|A|) \), \( B \preceq |B| \)** using ** eqpoll_sym , Card_cardinal , eqpoll_imp_lepoll
** with **AS ** have ** \( B\prec |A| \)** using ** lt_Card_imp_lesspoll , lesspoll_trans1
** then **** have ** I1: \( B\preceq |A| \)** using ** lesspoll_def
** from **B(1) ** have ** I2: \( A\preceq |A| \)** using ** eqpoll_sym , eqpoll_imp_lepoll
** have ** \( A \cup B\preceq A+B \)** using ** Un_lepoll_sum
** also ** ** from **I1, I2 ** have ** \( \ldots \preceq |A| + |A| \)** using ** sum_lepoll_mono
** also ** ** from **AG ** have ** \( \ldots \preceq |A| * |A| \)** using ** sum_lepoll_prod
** also ** ** from **INFB, assms(3) ** have ** \( \ldots \approx |A| \)** using ** InfCard_square_eqpoll
** finally **** have ** \( A \cup B\preceq |A| \)
** also ** ** from **TTT ** have ** \( \ldots \prec Q \)
** finally **** have ** \( A \cup B\prec Q \)
** } **
** moreover ** {
** assume **AS: \( |A|=|B| \)
** with **D ** have ** INFB: \( \text{InfCard}(|A|) \)
** then **** have ** \( 2 \lt |A| \)** using ** nat_less_infty
** then **** have ** AG: \( 2\preceq |A| \)** using ** lt_Card_imp_lesspoll , Card_cardinal** using ** lesspoll_def
** from **B(1) ** have ** \( |A|\approx A \)
** also ** ** from **assms(1) ** have ** \( \ldots \prec Q \)
** finally **** have ** TTT: \( |A|\prec Q \)
** from **AS, B ** have ** I1: \( A\preceq |A| \)** and **I2: \( B\preceq |A| \)** using ** eqpoll_refl , eqpoll_imp_lepoll , eqpoll_sym
** have ** \( A \cup B\preceq A+B \)** using ** Un_lepoll_sum
** also ** ** from **I1, I2 ** have ** \( \ldots \preceq |A| + |A| \)** using ** sum_lepoll_mono
** also ** ** from **AG ** have ** \( \ldots \preceq |A| * |A| \)** using ** sum_lepoll_prod
** also ** ** from **assms(3), INFB ** have ** \( \ldots \approx |A| \)** using ** InfCard_square_eqpoll
** finally **** have ** \( A \cup B\preceq |A| \)
** also ** ** from **TTT ** have ** \( \ldots \prec Q \)
** finally **** have ** \( A \cup B\prec Q \)
** } **
** ultimately **** have ** \( A \cup B\prec Q \)** using ** Ord_linear_lt_IML , Card_cardinal , Card_is_Ord
** } **
** ultimately **** show ** \( A \cup B\prec Q \)
** qed **

We want to prove some theorems assuming that some version of the Axiom of Choice holds. To avoid introducing it as an axiom we will defin an appropriate predicate and put that in the assumptions of the theorems. That way technically we stay inside ZF.

The first predicate we define states that the axiom of \(Q\)-choice holds for subsets of \(K\) if we can find a choice function for every family of subsets of \(K\) whose (that family's) cardinality does not exceed \(Q\).

** Definition **

\( \text{ the axiom of } Q \text{ choice holds for subsets }K \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq K)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)

Next we define a general form of \(Q\) choice where we don't require a collection of files to be included in a file.

** Definition **

\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)

The axiom of finite choice always holds.

** theorem ** finite_choice:

** assumes **\( n\in nat \)

The axiom of choice holds if and only if the *AxiomCardinalChoice*
holds for every couple of a cardinal *Q* and a set *K*.

** lemma ** choice_subset_imp_choice:

A choice axiom for greater cardinality implies one for smaller cardinality

** lemma ** greater_choice_imp_smaller_choice:

** assumes **\( Q\preceq Q1 \), \( \text{Card}(Q) \)

If we have a surjective function from a set which is injective to a set of ordinals, then we can find an injection which goes the other way.

** lemma ** surj_fun_inv:

** assumes **\( f \in \text{surj}(A,B) \), \( A\subseteq Q \), \( Ord(Q) \)

{
** fix **\( w \) \( x \)
** assume **AS: \( gw=gx \), \( w\in B \), \( x\in B \)
** from **assms(1), OA, AS(2,3) ** obtain **\( wz \) \( xz \)** where **P1: \( wz\in A \wedge f(wz)=w \), \( Ord(wz) \)** and **P2: \( xz\in A \wedge f(xz)=x \), \( Ord(xz) \)** unfolding ** surj_def
** from **P1 ** have ** \( (\ \lt mu> j.\ j\in A\wedge fj=w) \in A \wedge f(\ \lt mu> j.\ j\in A\wedge fj=w)=w \)** by (rule **LeastI** ) **
** moreover ** ** from **P2 ** have ** \( (\ \lt mu> j.\ j\in A\wedge fj=x) \in A \wedge f(\ \lt mu> j.\ j\in A\wedge fj=x)=x \)** by (rule **LeastI** ) **
** ultimately **** have ** R: \( f(\ \lt mu> j.\ j\in A\wedge fj=w)=w \), \( f(\ \lt mu> j.\ j\in A\wedge fj=x)=x \)
** from **AS ** have ** \( (\ \lt mu> j.\ j\in A\wedge f(j)=w)=(\ \lt mu> j.\ j\in A \wedge f(j)=x) \)** using ** apply_equality , fun2
** hence ** \( f(\ \lt mu> j.\ j\in A \wedge f(j)=w) = f(\ \lt mu> j.\ j\in A \wedge f(j)=x) \)
** with **R(1) ** have ** \( w = f(\ \lt mu> j.\ j\in A\wedge fj=x) \)
** with **R(2) ** have ** \( w=x \)
** } **
** hence ** \( \forall w\in B.\ \forall x\in B.\ g(w) = g(x) \longrightarrow w = x \)
** with **fun2 ** show ** \( g\in \text{inj}(B,A) \)** unfolding ** inj_def
** qed **

The difference with the previous result is that in this one
*A* is not a subset of an ordinal, it is only injective
with one.

** theorem ** surj_fun_inv_2:

** assumes **\( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)

Definition of LimitC:
\( \text{LimitC}(i) \equiv \text{Card}(i) \wedge 0 \lt i \wedge (\forall y.\ (y \lt i\wedge \text{Card}(y)) \longrightarrow \text{csucc}(y) \lt i) \)

** assumes **\( \text{Card}(Q) \)

** assumes **\( Ord(i) \), \( Ord(j) \)

** assumes **\( \text{Card}(j) \)** and **\( \text{InfCard}(\text{csucc}(j)) \)

Definition of AxiomCardinalChoiceGen:
\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)

** assumes **\( f \in \text{bij}(A,B) \)** and **\( a\in A \)

Definition of AxiomCardinalChoice:
\( \text{ the axiom of } Q \text{ choice holds for subsets }K \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq K)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)

** assumes **\( f=\{\langle x,g(x)\rangle .\ x\in X\} \)

** assumes **\( f \in \text{inj}(A,B) \)

** assumes **\( f \in \text{surj}(A,B) \), \( A\subseteq Q \), \( Ord(Q) \)