Theory Cardinal_ZF

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2012 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section ‹Cardinal numbers›

theory Cardinal_ZF imports ZF.CardinalArith func1

begin

text‹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.›

subsection‹Some new ideas on cardinals›

text‹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.›

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

definition
    "LimitC(i) ≡ Card(i) ∧ 0<i ∧ (∀y. (y<i∧Card(y)) ⟶ csucc(y)<i)"

text‹Simple fact used a couple of times in proofs.›

lemma nat_less_infty: assumes "n∈nat" and "InfCard(X)" shows "n<X"
proof -
  from assms have "n<nat" and "nat≤X" using lt_def InfCard_def by auto
  then show "n<X" using lt_trans2 by blast
qed

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

lemma Card_cases_disj: 
  assumes "Card(i)" 
  shows "i=0 | (∃j. Card(j) ∧ i=csucc(j)) | LimitC(i)"
proof-
  from assms have D: "Ord(i)" using Card_is_Ord by auto
  {
    assume F: "i≠0"
    assume Contr: "~LimitC(i)"
    from F D have "0<i" using Ord_0_lt by auto
    with Contr assms have "∃y. y < i ∧ Card(y) ∧ ¬ csucc(y) < i" 
      using LimitC_def by blast
    then obtain y where " y < i ∧ Card(y) ∧ ¬ csucc(y) < i"  by blast
    with D have " y < i" " i≤csucc(y)" and O: "Card(y)"
      using not_lt_imp_le lt_Ord Card_csucc Card_is_Ord
      by auto
    with assms have "csucc(y)≤i""i≤csucc(y)" using csucc_le by auto
    then have "i=csucc(y)" using le_anti_sym by auto
    with O have "∃j. Card(j) ∧ i=csucc(j)" by auto
  } thus ?thesis by auto
qed

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

lemma le_imp_lesspoll:
  assumes "Card(Q)"
  shows "A ≤ Q ⟹ A ≲ Q"
proof -
  assume "A ≤ Q"
  then have "A<Q∨A=Q" using le_iff by auto
  then have "A≈Q∨A< Q" using eqpoll_refl by auto
  with assms have "A≈Q∨A≺ Q" using lt_Card_imp_lesspoll by auto
  then show "A≲Q" using lesspoll_def eqpoll_imp_lepoll by auto
qed

text‹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 "InfCard(Q)"
  shows "Q=nat ∨ (∃j. csucc(j)≲Q ∧ InfCard(j))"
proof-
  {
    assume "∀j. ¬ csucc(j) ≲ Q ∨ ¬ InfCard(j)"
    then have D: "¬ csucc(nat) ≲ Q" using InfCard_nat by auto
    with D assms have "¬(csucc(nat) ≤ Q)" using le_imp_lesspoll InfCard_is_Card 
      by auto
    with assms have "Q<(csucc(nat))" 
      using not_le_iff_lt Card_is_Ord Card_csucc Card_is_Ord
        Card_is_Ord InfCard_is_Card Card_nat by auto  
    with assms have "Q≤nat" using Card_lt_csucc_iff InfCard_is_Card Card_nat 
      by auto
    with assms have "Q=nat" using InfCard_def le_anti_sym by auto
  }
  thus ?thesis by auto
qed

text‹A more readable version of standard Isabelle/ZF ‹Ord_linear_lt››

lemma Ord_linear_lt_IML: assumes "Ord(i)" "Ord(j)"
  shows "i<j ∨ i=j ∨ j<i"
  using assms lt_def Ord_linear disjE by simp 

text‹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 "Card(m)"
  shows "A ≺ csucc(m) ⟷ A ≲ m"
proof
  have S: "Ord(csucc(m))" using Card_csucc Card_is_Ord assms by auto
  {
    assume A: "A ≺ csucc(m)"
    with S have "|A|≈A" using lesspoll_imp_eqpoll by auto
    also from A have "…≺ csucc(m)" by auto
    finally have "|A|≺ csucc(m)" by auto
    then have "|A|≲csucc(m)""~(|A|≈csucc(m))" using lesspoll_def by auto
    with S have "||A||≤csucc(m)""|A|≠csucc(m)" using lepoll_cardinal_le by auto
    then have "|A|≤csucc(m)" "|A|≠csucc(m)" using Card_def Card_cardinal by auto
    then have I: "~(csucc(m)<|A|)" "|A|≠csucc(m)" using le_imp_not_lt by auto
    from S have "csucc(m)<|A| ∨ |A|=csucc(m) ∨ |A|<csucc(m)"
      using Card_cardinal Card_is_Ord Ord_linear_lt_IML by auto 
    with I have "|A|<csucc(m)" by simp     
    with assms have "|A|≤m" using Card_lt_csucc_iff Card_cardinal
      by auto
    then have "|A|=m∨ |A|< m" using le_iff by auto
    then have "|A|≈m∨|A|< m" using eqpoll_refl by auto
    then have "|A|≈m∨|A|≺ m" using lt_Card_imp_lesspoll assms by auto
    then have T:"|A|≲m" using lesspoll_def eqpoll_imp_lepoll by auto
    from A S have "A≈|A|" using lesspoll_imp_eqpoll eqpoll_sym by auto
    also from T have "…≲m" by auto
    finally show "A≲m" by simp
  }
  {
    assume A: "A≲m"
    from assms have "m≺csucc(m)" using lt_Card_imp_lesspoll Card_csucc Card_is_Ord
      lt_csucc by auto
    with A show "A≺csucc(m)" using lesspoll_trans1 by auto
  }
qed

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

lemma csucc_inf_imp_inf:
  assumes "Card(j)" and "InfCard(csucc(j))"
  shows "InfCard(j)"
proof-
  {
    assume f:"Finite (j)"
    then obtain n where "n∈nat" "j≈n" using Finite_def by auto
    with assms(1) have TT: "j=n" "n∈nat" 
      using cardinal_cong nat_into_Card Card_def by auto
    then have Q:"succ(j)∈nat" using nat_succI by auto
    with f TT have T: "Finite(succ(j))" "Card(succ(j))" 
      using nat_into_Card nat_succI by auto 
    from T(2) have "Card(succ(j))∧ j<succ(j)" using Card_is_Ord by auto
    moreover from this have "Ord(succ(j))" using Card_is_Ord by auto
    moreover
    { fix x
      assume A: "x<succ(j)"
      {
        assume "Card(x)∧ j<x"
        with A have "False" using lt_trans1 by auto
      }
      hence "~(Card(x)∧ j<x)" by auto
    } 
    ultimately have "(μ L. Card(L) ∧ j < L)=succ(j)"
      by (rule Least_equality)
    then have "csucc(j)=succ(j)" using csucc_def by auto
    with Q have "csucc(j)∈nat" by auto
    then have "csucc(j)<nat" using lt_def Card_nat Card_is_Ord by auto
    with assms(2) have "False" using InfCard_def lt_trans2 by auto
  }
  then have "~(Finite (j))" by auto
  with assms(1) show ?thesis using Inf_Card_is_InfCard by auto
qed

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

corollary LimitC_nat:
  shows "LimitC(nat)"
proof-
  note Card_nat
  moreover have "0<nat" using lt_def by auto
  moreover
  {
    fix y
    assume AS: "y<nat""Card(y)"
    then have ord: "Ord(y)" unfolding lt_def by auto
    then have Cacsucc: "Card(csucc(y))" using Card_csucc by auto
    {
      assume "nat≤csucc(y)"
      with Cacsucc have "InfCard(csucc(y))" using InfCard_def by auto
      with AS(2) have "InfCard(y)" using csucc_inf_imp_inf by auto
      then have "nat≤y" using InfCard_def by auto
      with AS(1) have "False" using lt_trans2 by auto
    }
    hence "~(nat≤csucc(y))" by auto
    then have "csucc(y)<nat" using not_le_iff_lt Ord_nat Cacsucc Card_is_Ord by auto
  }
  ultimately show ?thesis using LimitC_def by auto
qed

subsection‹Main result on cardinals (without the Axiom of Choice)›

text‹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 ‹LimitC(Q)› and it also makes use
of the Axiom of Choice. The mentioned theorem is in the
theory file ‹Cardinal_AC.thy››

text‹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≺Q" and "B≺Q" and "InfCard(Q)"
  shows "A ∪ B≺Q"
proof-
{
  assume "Finite (A) ∧ Finite(B)"
  then have "Finite(A ∪ B)" using Finite_Un by auto
  then obtain n where R: "A ∪ B ≈n"  "n∈nat" using Finite_def
    by auto
  then have "|A ∪ B|<nat" using lt_def  cardinal_cong
    nat_into_Card  Card_def  Card_nat Card_is_Ord by auto
  with assms(3) have T: "|A ∪ B|<Q" using InfCard_def lt_trans2 by auto
  from R have "Ord(n)""A ∪ B ≲ n" using nat_into_Card Card_is_Ord eqpoll_imp_lepoll by auto
  then have "A ∪ B≈|A ∪ B|" using lepoll_Ord_imp_eqpoll eqpoll_sym by auto
  also from T assms(3) have "…≺Q" using lt_Card_imp_lesspoll InfCard_is_Card
    by auto
  finally have "A ∪ B≺Q" by simp
}
moreover
{
  assume "~(Finite (A) ∧ Finite(B))"
  hence A: "~Finite (A) ∨ ~Finite(B)" by auto
  from assms have B: "|A|≈A" "|B|≈B" using lesspoll_imp_eqpoll lesspoll_imp_eqpoll
    InfCard_is_Card Card_is_Ord by auto
  from B(1) have Aeq: "∀x. (|A|≈x) ⟶ (A≈x)"
    using eqpoll_sym eqpoll_trans by blast
  from B(2) have Beq: "∀x. (|B|≈x) ⟶ (B≈x)"
    using eqpoll_sym eqpoll_trans by blast
  with A Aeq have "~Finite(|A|)∨ ~Finite(|B|)" using Finite_def
    by auto
  then have D: "InfCard(|A|)∨InfCard(|B|)" 
    using Inf_Card_is_InfCard Inf_Card_is_InfCard  Card_cardinal by blast
  {
    assume AS: "|A| < |B|"
    {
      assume "~InfCard(|A|)"
      with D have "InfCard(|B|)" by auto
    }
    moreover
    {
      assume "InfCard(|A|)"
      then have "nat≤|A|" using InfCard_def by auto
      with AS have "nat<|B|" using lt_trans1 by auto
      then have "nat≤|B|" using leI by auto
      then have "InfCard(|B|)" using InfCard_def Card_cardinal by auto
    }
    ultimately have INFB: "InfCard(|B|)" by auto
    then have "2<|B|" using nat_less_infty by simp 
    then have AG: "2≲|B|" using lt_Card_imp_lesspoll Card_cardinal lesspoll_def
      by auto
    from B(2) have "|B|≈B" by simp 
    also from assms(2) have "…≺Q" by auto
    finally have TTT: "|B|≺Q" by simp 
    from B(1) have "Card(|B|)" "A ≲|A|" using eqpoll_sym Card_cardinal eqpoll_imp_lepoll 
      by auto
    with AS have "A≺|B|" using  lt_Card_imp_lesspoll lesspoll_trans1 by auto
    then have I1: "A≲|B|" using lesspoll_def by auto
    from B(2) have I2: "B≲|B|" using  eqpoll_sym eqpoll_imp_lepoll by auto
    have "A ∪ B≲A+B" using Un_lepoll_sum by auto
    also from I1 I2 have "…≲ |B| + |B|" using sum_lepoll_mono by auto
    also from AG have "…≲|B| * |B|" using sum_lepoll_prod by auto
    also from assms(3) INFB have "…≈|B|" using InfCard_square_eqpoll
      by auto
    finally have "A ∪ B≲|B|" by simp
    also from TTT have "…≺Q" by auto
    finally have "A ∪ B≺Q" by simp 
  }
  moreover
  {
    assume AS: "|B| < |A|"
    {
      assume "~InfCard(|B|)"
      with D have "InfCard(|A|)" by auto
    }
    moreover
    {
      assume "InfCard(|B|)"
      then have "nat≤|B|" using InfCard_def by auto
      with AS have "nat<|A|" using lt_trans1 by auto
      then have "nat≤|A|" using leI by auto
      then have "InfCard(|A|)" using InfCard_def Card_cardinal by auto
    }
    ultimately have INFB: "InfCard(|A|)" by auto
    then have "2<|A|" using nat_less_infty by simp
    then have AG: "2≲|A|" using lt_Card_imp_lesspoll Card_cardinal lesspoll_def
        by auto
    from B(1) have "|A|≈A" by simp
    also from assms(1) have "…≺Q" by auto
    finally have TTT: "|A|≺Q" by simp
    from B(2) have "Card(|A|)" "B ≲|B|" using eqpoll_sym Card_cardinal eqpoll_imp_lepoll 
      by auto
    with AS have "B≺|A|" using  lt_Card_imp_lesspoll lesspoll_trans1 by auto
    then have I1: "B≲|A|" using lesspoll_def by auto
    from B(1) have I2: "A≲|A|" using eqpoll_sym eqpoll_imp_lepoll by auto
    have "A ∪ B≲A+B" using Un_lepoll_sum by auto
    also from I1 I2 have "…≲ |A| + |A|" using sum_lepoll_mono by auto
    also from AG have "…≲|A| * |A|" using sum_lepoll_prod by auto
    also from INFB assms(3) have "…≈|A|" using InfCard_square_eqpoll
       by auto
    finally have "A ∪ B≲|A|" by simp
    also from TTT have "…≺Q" by auto
    finally have "A ∪ B≺Q" by simp 
    }
    moreover
    {
      assume AS: "|A|=|B|"
      with D have INFB: "InfCard(|A|)" by auto
      then have "2<|A|" using nat_less_infty by simp
      then have AG: "2≲|A|" using lt_Card_imp_lesspoll Card_cardinal using lesspoll_def
        by auto
      from B(1) have "|A|≈A" by simp 
      also from assms(1) have "…≺Q" by auto
      finally have TTT: "|A|≺Q" by simp
      from AS B have I1: "A≲|A|"and I2:"B≲|A|" using eqpoll_refl eqpoll_imp_lepoll
        eqpoll_sym by auto
      have "A ∪ B≲A+B" using Un_lepoll_sum by auto
      also from I1 I2 have "…≲ |A| + |A|" using sum_lepoll_mono by auto
      also from AG have "…≲|A| * |A|" using sum_lepoll_prod  by auto
      also from assms(3) INFB have "…≈|A|" using InfCard_square_eqpoll
        by auto
      finally have "A ∪ B≲|A|" by simp 
      also from TTT have "…≺Q" by auto
      finally have "A ∪ B≺Q" by simp
    }
    ultimately have "A ∪ B≺Q" using Ord_linear_lt_IML Card_cardinal Card_is_Ord by auto
  }
  ultimately show "A ∪ B≺Q" by auto
qed

subsection‹Choice axioms›

text‹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.›

text‹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
  AxiomCardinalChoice ("{the axiom of}_{choice holds for subsets}_") where
  "{the axiom of} Q {choice holds for subsets}K ≡ Card(Q) ∧ (∀ M N. (M ≲Q ∧  (∀t∈M. N`t≠0 ∧ N`t⊆K)) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t)))"

text‹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
  AxiomCardinalChoiceGen ("{the axiom of}_{choice holds}") where
  "{the axiom of} Q {choice holds} ≡ Card(Q) ∧ (∀ M N. (M ≲Q ∧  (∀t∈M. N`t≠0)) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t)))"

text‹The axiom of finite choice always holds.›

theorem finite_choice:
  assumes "n∈nat"
  shows "{the axiom of} n {choice holds}"
proof -
  note assms(1)
  moreover
  {
    fix M N assume "M≲0" "∀t∈M. N`t≠0"
    then have "M=0" using lepoll_0_is_0 by auto
    then have "{⟨t,0⟩. t∈M}:Pi(M,λt. N`t)" unfolding Pi_def domain_def function_def Sigma_def by auto
    moreover from ‹M=0› have "∀t∈M. {⟨t,0⟩. t∈M}`t∈N`t" by auto
    ultimately have "(∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" by auto
  }
  then have "(∀ M N. (M ≲0 ∧  (∀t∈M. N`t≠0)) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t)))" 
    by auto
  then have "{the axiom of} 0 {choice holds}" using AxiomCardinalChoiceGen_def nat_into_Card 
    by auto
  moreover { 
    fix x
    assume as: "x∈nat" "{the axiom of} x {choice holds}"
    {
      fix M N assume ass: "M≲succ(x)" "∀t∈M. N`t≠0"
      {
        assume "M≲x"
        from as(2) ass(2) have 
          "(M ≲ x ∧ (∀t∈M. N ` t ≠ 0)) ⟶ (∃f. f ∈ Pi(M,λt. N ` t) ∧ (∀t∈M. f ` t ∈ N ` t))" 
            unfolding AxiomCardinalChoiceGen_def by auto
        with ‹M≲x› ass(2) have "(∃f. f ∈ Pi(M,λt. N ` t) ∧ (∀t∈M. f ` t ∈ N ` t))" 
          by auto
      }
      moreover
      {
        assume "M≈succ(x)"
        then obtain f where f:"f∈bij(succ(x),M)" using eqpoll_sym eqpoll_def by blast 
        moreover
        have "x∈succ(x)" unfolding succ_def by auto
        ultimately have "restrict(f,succ(x)-{x})∈bij(succ(x)-{x},M-{f`x})" using bij_restrict_rem 
          by auto 
        moreover
        have "x∉x" using mem_not_refl by auto
        then have "succ(x)-{x}=x" unfolding succ_def by auto
        ultimately have "restrict(f,x)∈bij(x,M-{f`x})" by auto
        then have "x≈M-{f`x}" unfolding eqpoll_def by auto
        then have "M-{f`x}≈x" using eqpoll_sym by auto
        then have "M-{f`x}≲x" using eqpoll_imp_lepoll by auto
        with as(2) ass(2) have "(∃g. g ∈ Pi(M-{f`x},λt. N ` t) ∧ (∀t∈M-{f`x}. g ` t ∈ N ` t))" 
          unfolding AxiomCardinalChoiceGen_def by auto
        then obtain g where g: "g∈ Pi(M-{f`x},λt. N ` t)" "∀t∈M-{f`x}. g ` t ∈ N ` t" 
          by auto
        from f have ff: "f`x∈M" using bij_def inj_def apply_funtype by auto
        with ass(2) have "N`(f`x)≠0" by auto
        then obtain y where y: "y∈N`(f`x)" by auto
        from g(1) have gg: "g⊆Sigma(M-{f`x},(`)(N))" unfolding Pi_def by auto
        with y ff have "g ∪{⟨f`x, y⟩}⊆Sigma(M, (`)(N))" unfolding Sigma_def by auto 
        moreover
        from g(1) have dom: "M-{f`x}⊆domain(g)" unfolding Pi_def by auto
        then have "M⊆domain(g ∪{⟨f`x, y⟩})" unfolding domain_def by auto 
        moreover
        from gg g(1) have noe: "~(∃t. ⟨f`x,t⟩∈g)" and "function(g)"
          unfolding domain_def Pi_def Sigma_def by auto  
        with dom have fg: "function(g ∪{⟨f`x, y⟩})" unfolding function_def by blast 
        ultimately have PP: "g ∪{⟨f`x, y⟩}∈Pi(M,λt. N ` t)" unfolding Pi_def by auto
        have "⟨f`x, y⟩ ∈ g ∪{⟨f`x, y⟩}" by auto
        from this fg have "(g ∪{⟨f`x, y⟩})`(f`x)=y" by (rule function_apply_equality)
        with y have "(g ∪{⟨f`x, y⟩})`(f`x)∈N`(f`x)" by auto 
        moreover
        {
          fix t assume A:"t∈M-{f`x}"
          with g(1) have "⟨t,g`t⟩∈g" using apply_Pair by auto
          then have "⟨t,g`t⟩∈(g ∪{⟨f`x, y⟩})" by auto
          then have "(g ∪{⟨f`x, y⟩})`t=g`t" using apply_equality PP by auto
          with A have "(g ∪{⟨f`x, y⟩})`t∈N`t" using g(2) by auto
        }
        ultimately have "∀t∈M. (g ∪{⟨f`x, y⟩})`t∈N`t" by auto
        with PP have "∃g. g∈Pi(M,λt. N ` t) ∧ (∀t∈M. g`t∈N`t)" by auto
      }
    ultimately have "∃g. g ∈ Pi(M, λt. N`t) ∧ (∀t∈M. g ` t ∈ N ` t)" using as(1) ass(1)
      lepoll_succ_disj by auto
    }
    then have "∀M N. M ≲ succ(x)∧(∀t∈M. N`t≠0)⟶(∃g. g ∈ Pi(M,λt. N ` t) ∧ (∀t∈M. g ` t ∈ N ` t))" 
      by auto
    then have "{the axiom of}succ(x){choice holds}" 
      using AxiomCardinalChoiceGen_def nat_into_Card as(1) nat_succI by auto
  }
  ultimately show ?thesis by (rule nat_induct)
qed

text‹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:
  shows "{the axiom of} Q {choice holds} ⟷ (∀ K. {the axiom of} Q {choice holds for subsets}K)"
  unfolding AxiomCardinalChoice_def AxiomCardinalChoiceGen_def by blast

text‹A choice axiom for greater cardinality implies one for 
smaller cardinality›

lemma greater_choice_imp_smaller_choice:
  assumes "Q≲Q1" "Card(Q)"
  shows "{the axiom of} Q1 {choice holds} ⟶ ({the axiom of} Q {choice holds})" using assms
  AxiomCardinalChoiceGen_def lepoll_trans by auto   

text‹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 ∈ surj(A,B)" "A⊆Q" "Ord(Q)"
  shows "B≲A"
proof-
  let ?g = "{⟨m,μ j. j∈A ∧ f`(j)=m⟩. m∈B}" 
  have "?g:B→range(?g)" using lam_is_fun_range by simp
  then have fun: "?g:B→?g``(B)" using range_image_domain by simp
  from assms(2,3) have OA: "∀j∈A. Ord(j)" using lt_def Ord_in_Ord by auto
  {
    fix x
    assume "x∈?g``(B)"
    then have "x∈range(?g)" and "∃y∈B. ⟨y,x⟩∈?g" by auto
    then obtain y where T: "x=(μ j. j∈A∧ f`(j)=y)" and "y∈B" by auto
    with assms(1) OA obtain z where P: "z∈A ∧ f`(z)=y" "Ord(z)" unfolding surj_def 
      by auto
    with T have "x∈A ∧ f`(x)=y" using LeastI by simp  
    hence "x∈A" by simp
  }
  then have "?g``(B) ⊆ A" by auto
  with fun have fun2: "?g:B→A" using fun_weaken_type by auto
  then have "?g∈inj(B,A)" 
  proof -
    {
      fix w x
      assume AS: "?g`w=?g`x" "w∈B" "x∈B"
      from assms(1) OA AS(2,3) obtain wz xz where 
        P1: "wz∈A ∧ f`(wz)=w"  "Ord(wz)" and P2: "xz∈A ∧ f`(xz)=x"  "Ord(xz)" 
        unfolding surj_def by blast
      from P1 have "(μ j. j∈A∧ f`j=w) ∈ A ∧ f`(μ j. j∈A∧ f`j=w)=w" 
        by (rule LeastI)
      moreover from P2 have "(μ j. j∈A∧ f`j=x) ∈ A ∧ f`(μ j. j∈A∧ f`j=x)=x"
        by (rule LeastI) 
      ultimately have R: "f`(μ j. j∈A∧ f`j=w)=w" "f`(μ j. j∈A∧ f`j=x)=x" 
        by auto
      from AS have "(μ j. j∈A∧ f`(j)=w)=(μ j. j∈A ∧ f`(j)=x)" 
        using apply_equality fun2 by auto
      hence "f`(μ j. j∈A ∧ f`(j)=w) = f`(μ j. j∈A ∧ f`(j)=x)" by auto
      with R(1) have "w = f`(μ j. j∈A∧ f`j=x)" by auto
      with R(2) have "w=x" by auto
    }
    hence "∀w∈B. ∀x∈B. ?g`(w) = ?g`(x) ⟶ w = x" 
      by auto 
    with fun2 show "?g∈inj(B,A)" unfolding inj_def by auto     
  qed
  then show ?thesis unfolding lepoll_def by auto
qed

text‹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:surj(A,B)" "A≲Q" "Ord(Q)"
  shows "B≲A"
proof-
  from assms(2) obtain h where h_def: "h∈inj(A,Q)" using lepoll_def by auto
  then have bij: "h∈bij(A,range(h))" using inj_bij_range by auto
  then obtain h1 where "h1∈bij(range(h),A)" using bij_converse_bij by auto
  then have "h1 ∈ surj(range(h),A)" using bij_def by auto
  with assms(1) have "(f O h1)∈surj(range(h),B)" using comp_surj by auto
  moreover
  {
    fix x
    assume p: "x∈range(h)"
    from bij have "h∈surj(A,range(h))" using bij_def by auto
    with p obtain q where "q∈A" and "h`(q)=x" using surj_def by auto
    then have "x∈Q" using h_def inj_def by auto
  }
  then have "range(h)⊆Q" by auto
  ultimately have "B≲range(h)" using surj_fun_inv assms(3) by auto
  moreover have "range(h)≈A" using bij eqpoll_def eqpoll_sym by blast
  ultimately show "B≲A" using lepoll_eq_trans by auto
qed


end