(* 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