Theory Topology_ZF_properties

theory Topology_ZF_properties
imports Topology_ZF_examples Topology_ZF_examples_1
(* 
    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 ‹Properties in Topology›

theory Topology_ZF_properties imports Topology_ZF_examples Topology_ZF_examples_1

begin

text{*
  This theory deals with topological properties which make use of cardinals.
  *}

subsection{*Properties of compactness*}

text{*It is already defined what is a compact topological space, but the is a
generalization which may be useful sometimes.*}

definition
  IsCompactOfCard ("_{is compact of cardinal}_ {in}_" 90)
  where "K{is compact of cardinal} Q{in}T ≡ (Card(Q) ∧ K ⊆ ⋃T ∧ 
  (∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺Q)))"

text{*The usual compact property is the one defined over the cardinal
of the natural numbers.*}

lemma Compact_is_card_nat:
  shows "K{is compact in}T ⟷ (K{is compact of cardinal} nat {in}T)"
proof
  {
    assume "K{is compact in}T"
    then have sub:"K ⊆ ⋃T"  and reg:"(∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ FinPow(M). K ⊆ ⋃N))"
      using IsCompact_def by auto
    {
      fix M
      assume "M∈Pow(T)""K⊆⋃M"
      with reg obtain N where "N∈FinPow(M)" "K⊆⋃N" by blast
      then have "Finite(N)" using FinPow_def by auto
      then obtain n where A:"n∈nat""N ≈n" using Finite_def by auto
      from A(1) have "n≺nat" using n_lesspoll_nat by auto
      with A(2) have "N≲nat" using lesspoll_def eq_lepoll_trans by auto
      moreover
      {
        assume "N ≈nat"
        then have "nat ≈ N" using eqpoll_sym by auto 
        with A(2) have "nat ≈n" using eqpoll_trans by blast
        then have "n ≈nat" using eqpoll_sym by auto
        with `n≺nat` have "False" using lesspoll_def by auto
      }
      then have "~(N ≈nat)" by auto
      with calculation `K⊆⋃N``N∈FinPow(M)` have "N≺nat""K⊆⋃N""N∈Pow(M)" using lesspoll_def
        FinPow_def by auto
      hence "(∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat)" by auto
    }
    with sub show "K{is compact of cardinal} nat {in}T" using IsCompactOfCard_def Card_nat by auto
  }
  {
    assume "(K{is compact of cardinal} nat {in}T)"
    then have sub:"K⊆⋃T" and reg:"(∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat))"
      using IsCompactOfCard_def by auto
    {
      fix M
      assume "M∈Pow(T)""K⊆⋃M"
      with reg have "(∃ N ∈ Pow(M). K ⊆ ⋃N ∧ N≺nat)" by auto
      then obtain N where "N∈Pow(M)""K⊆⋃N""N≺nat" by blast
      then have "N∈FinPow(M)""K⊆⋃N" using lesspoll_nat_is_Finite FinPow_def by auto
      hence "∃N∈FinPow(M). K⊆⋃N" by auto
    }
    with sub show "K{is compact in}T" using IsCompact_def by auto
  }
qed

text{*Another property of this kind widely used is the Lindeloef property;
it is the one on the successor of the natural numbers.*}

definition
  IsLindeloef  ("_{is lindeloef in}_" 90) where
  "K {is lindeloef in} T≡K{is compact of cardinal}csucc(nat){in}T"

text{*It would be natural to think that every countable set with any topology
is Lindeloef; but this statement is not provable in ZF. The reason is that
to build a subcover, most of the time we need to \emph{choose} sets
from an infinite collection which cannot be done in ZF. Additional axioms are needed,
but strictly weaker than the axiom of choice.*}

text{*However, if the topology has not many open sets, then the topological
space is indeed compact.*}

theorem card_top_comp:
  assumes "Card(Q)" "T≺Q" "K⊆⋃T"
  shows "(K){is compact of cardinal}Q{in}T"
proof-
  {      
    fix M assume M:"M⊆T" "K⊆⋃M"
    from M(1) assms(2) have "M≺Q" using subset_imp_lepoll lesspoll_trans1 by blast
    with M(2) have "∃N∈Pow(M). K⊆⋃N ∧ N≺Q" by auto
  }
  with assms(1,3) show ?thesis unfolding IsCompactOfCard_def by auto
qed

text{*The union of two compact sets, is compact; of any cardinality.*}

theorem union_compact:
  assumes "K{is compact of cardinal}Q{in}T" "K1{is compact of cardinal}Q{in}T" "InfCard(Q)"
  shows "(K ∪ K1){is compact of cardinal}Q{in}T" unfolding IsCompactOfCard_def
proof(safe)
  from assms(1) show "Card(Q)" unfolding IsCompactOfCard_def by auto
  fix x assume "x∈K" then show "x∈⋃T" using assms(1) unfolding IsCompactOfCard_def by blast
next
  fix x assume "x∈K1" then show "x∈⋃T" using assms(2) unfolding IsCompactOfCard_def by blast
next
  fix M assume "M⊆T" "K∪K1⊆⋃M"
  then have "K⊆⋃M""K1⊆⋃M" by auto
  with `M⊆T` have "∃N∈Pow(M). K ⊆ ⋃N ∧ N ≺ Q""∃N∈Pow(M). K1 ⊆ ⋃N ∧ N ≺ Q" using assms unfolding IsCompactOfCard_def
    by auto
  then obtain NK NK1 where "NK∈Pow(M)""NK1∈Pow(M)""K ⊆ ⋃NK""K1 ⊆ ⋃NK1""NK ≺ Q""NK1 ≺ Q" by auto
  then have "NK∪NK1 ≺ Q""K∪K1⊆⋃(NK∪NK1)""NK∪NK1∈Pow(M)" using assms(3) less_less_imp_un_less by auto
  then show "∃N∈Pow(M). K∪K1⊆⋃N ∧ N≺Q" by auto
qed

text{*If a set is compact of cardinality @{text "Q"} for some topology,
it is compact of cardinality @{text "Q"} for every coarser topology.*}

theorem compact_coarser:
  assumes "T1⊆T" and "⋃T1=⋃T" and "(K){is compact of cardinal}Q{in}T"
  shows "(K){is compact of cardinal}Q{in}T1"
proof-
  {
    fix M
    assume AS:"M∈Pow(T1)""K⊆⋃M"
    then have "M∈Pow(T)""K⊆⋃M" using assms(1) by auto
    then have "∃N∈Pow(M).K⊆⋃N∧N≺Q" using assms(3) unfolding IsCompactOfCard_def by auto
  }
  then show "(K){is compact of cardinal}Q{in}T1" using assms(3,2) unfolding IsCompactOfCard_def by auto
qed

text{*If some set is compact for some cardinal, it is compact for any greater cardinal.*}

theorem compact_greater_card:
  assumes "Q≲Q1" and "(K){is compact of cardinal}Q{in}T" and "Card(Q1)"
  shows "(K){is compact of cardinal}Q1{in}T"
proof-
  {
    fix M
    assume AS: "M∈Pow(T)""K⊆⋃M"
    then have "∃N∈Pow(M).K⊆⋃N∧N≺Q" using assms(2) unfolding IsCompactOfCard_def by auto
    then have "∃N∈Pow(M).K⊆⋃N∧N≺Q1" using assms(1) lesspoll_trans2
      unfolding IsCompactOfCard_def by auto
  }
  then show ?thesis using assms(2,3) unfolding IsCompactOfCard_def by auto
qed

text{*A closed subspace of a compact space of any cardinality, is also
compact of the same cardinality.*}

theorem compact_closed:
  assumes "K {is compact of cardinal} Q {in} T"
    and "R {is closed in} T"
  shows "(K∩R) {is compact of cardinal} Q {in} T"
proof-
  {
    fix M
    assume AS:"M∈Pow(T)""K∩R⊆⋃M"
    have "⋃T-R∈T" using assms(2) IsClosed_def by auto
    have "K-R⊆(⋃T-R)" using assms(1) IsCompactOfCard_def by auto
    with `⋃T-R∈T` have "K⊆⋃(M ∪{⋃T-R})" and "M ∪{⋃T-R}∈Pow(T)"
    proof (safe)
      {
        fix x
        assume "x∈M"
        with AS(1) show "x∈T" by auto
      }
      {
        fix x
        assume "x∈K"
        have "x∈R∨x∉R" by auto
        with `x∈K` have "x∈K∩R∨x∈K-R" by auto
        with AS(2) `K-R⊆(⋃T-R)` have "x∈⋃M∨x∈(⋃T-R)" by auto
        then show "x∈⋃(M ∪{⋃T-R})" by auto
      }
    qed
    with assms(1) have "∃N∈Pow(M∪{⋃T-R}). K ⊆ ⋃N ∧ N ≺ Q" unfolding IsCompactOfCard_def by auto
    then obtain N where cub:"N∈Pow(M∪{⋃T-R})" "K⊆⋃N" "N≺Q" by auto
    have "N-{⋃T-R}∈Pow(M)""K∩R⊆⋃(N-{⋃T-R})" "N-{⋃T-R}≺Q"
    proof (safe)
      {
        fix x
        assume "x∈N""x∉M"
        then show "x=⋃T-R" using cub(1) by auto
      }
      {
        fix x
        assume "x∈K""x∈R"
        then have "x∉⋃T-R""x∈K" by auto
        then show "x∈⋃(N-{⋃T-R})" using cub(2) by blast
      }
      have "N-{⋃T-R}⊆N" by auto
      with cub(3) show "N-{⋃T-R}≺Q" using subset_imp_lepoll lesspoll_trans1 by blast
    qed
    then have "∃N∈Pow(M). K∩R⊆⋃N ∧ N≺Q" by auto
  }
  then have "∀M∈Pow(T). (K ∩ R ⊆ ⋃M ⟶ (∃N∈Pow(M). K ∩ R ⊆ ⋃N ∧ N ≺ Q))" by auto
  then show ?thesis using IsCompactOfCard_def assms(1) by auto
qed

subsection{*Properties of numerability*}

text{*The properties of numerability deal with cardinals of some sets
built from the topology. The properties which are normally used
are the ones related to the cardinal of the natural numbers or its successor.*}

definition
  IsFirstOfCard ("_ {is of first type of cardinal}_" 90) where
  "(T {is of first type of cardinal} Q) ≡ ∀x∈⋃T. (∃B. (B {is a base for} T) ∧ ({b∈B. x∈b} ≺ Q))"

definition
  IsSecondOfCard ("_ {is of second type of cardinal}_" 90) where
  "(T {is of second type of cardinal}Q) ≡ (∃B. (B {is a base for} T) ∧ (B ≺ Q))"

definition
  IsSeparableOfCard ("_{is separable of cardinal}_" 90) where
  "T{is separable of cardinal}Q≡ ∃U∈Pow(⋃T). Closure(U,T)=⋃T ∧ U≺Q"

definition
  IsFirstCountable ("_ {is first countable}" 90) where
  "(T {is first countable}) ≡ T {is of first type of cardinal} csucc(nat)"

definition
  IsSecondCountable ("_ {is second countable}" 90) where
  "(T {is second countable}) ≡ (T {is of second type of cardinal}csucc(nat))"

definition
  IsSeparable ("_{is separable}" 90) where
  "T{is separable}≡ T{is separable of cardinal}csucc(nat)"

text{*If a set is of second type of cardinal @{text "Q"}, then it is of
first type of that same cardinal.*}

theorem second_imp_first:
  assumes "T{is of second type of cardinal}Q"
  shows "T{is of first type of cardinal}Q"
proof-
  from assms have "∃B. (B {is a base for} T) ∧ (B ≺ Q)" using IsSecondOfCard_def by auto
  then obtain B where base:"(B {is a base for} T) ∧ (B ≺ Q)" by auto
  {
    fix x
    assume "x∈⋃T"
    have "{b∈B. x∈b}⊆B" by auto
    then have "{b∈B. x∈b}≲B" using subset_imp_lepoll by auto
    with base have "{b∈B. x∈b}≺Q" using lesspoll_trans1 by auto
    with base have "(B {is a base for} T) ∧ {b∈B. x∈b}≺Q" by auto
  }
  then have "∀x∈⋃T. ∃B. (B {is a base for} T) ∧ {b∈B. x∈b}≺Q" by auto
  then show ?thesis using IsFirstOfCard_def by auto
qed

text{*A set is dense iff it intersects all non-empty, open sets of the topology.*}

lemma dense_int_open:
  assumes "T{is a topology}" and "A⊆⋃T"
  shows "Closure(A,T)=⋃T ⟷ (∀U∈T. U≠0 ⟶ A∩U≠0)"
proof
  assume AS:"Closure(A,T)=⋃T"
  {
    fix U
    assume Uopen:"U∈T" and "U≠0"
    then have "U∩⋃T≠0" by auto
    with AS have "U∩Closure(A,T) ≠0" by auto
    with assms Uopen have "U∩A≠0" using topology0.cl_inter_neigh topology0_def by blast
  }
  then show "∀U∈T. U≠0 ⟶ A∩U≠0" by auto
  next
  assume AS:"∀U∈T. U≠0 ⟶ A∩U≠0"
  {
    fix x
    assume A:"x∈⋃T"
    then have "∀U∈T. x∈U ⟶ U∩A≠0" using AS by auto
    with assms A have "x∈Closure(A,T)" using topology0.inter_neigh_cl topology0_def by auto
  }
  then have "⋃T⊆Closure(A,T)" by auto
  with assms show "Closure(A,T)=⋃T" using topology0.Top_3_L11(1) topology0_def by blast
qed

subsection{*Relations between numerability properties and choice principles*}

text{*It is known that some statements in topology aren't just derived from
choice axioms, but also equivalent to them. Here is an example

The following are equivalent:
\begin{itemize}
\item Every topological space of second cardinality @{text "csucc(Q)"} is
separable of cardinality @{text "csucc(Q)"}.
\item The axiom of @{text "Q"} choice.
\end{itemize}

In the article \cite{HH1} there is a proof of this statement
for @{text "Q"}$=\mathbb{N}$, with more equivalences.*}

text{*If a topology is of second type of cardinal @{text "csucc(Q)"}, then it is separable
of the same cardinal. This result makes use of the axiom of choice for the cardinal
 @{text "Q"} on subsets of @{text "⋃T"}.*}

theorem Q_choice_imp_second_imp_separable:
  assumes "T{is of second type of cardinal}csucc(Q)" 
    and "{the axiom of} Q {choice holds for subsets} ⋃T"
    and "T{is a topology}"
  shows "T{is separable of cardinal}csucc(Q)"
proof-
  from assms(1) have "∃B. (B {is a base for} T) ∧ (B ≺ csucc(Q))" using IsSecondOfCard_def by auto
  then obtain B where base:"(B {is a base for} T) ∧ (B ≺ csucc(Q))" by auto
  let ?N="λb∈B. b"
  let ?B="B-{0}"
  have "B-{0}⊆B" by auto
  with base have prec:"B-{0}≺csucc(Q)" using subset_imp_lepoll lesspoll_trans1 by blast
  from base have baseOpen:"∀b∈B. ?N`b∈T" using base_sets_open by auto
  from assms(2) have car:"Card(Q)" and reg:"(∀ M N. (M ≲Q ∧  (∀t∈M. N`t≠0 ∧ N`t⊆⋃T)) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t)))"
  using AxiomCardinalChoice_def by auto
  then have "(?B ≲Q ∧  (∀t∈?B. ?N`t≠0 ∧ ?N`t⊆⋃T)) ⟶ (∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t))" by blast
  with prec have "(∀t∈?B. ?N`t⊆⋃T) ⟶ (∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t))" using Card_less_csucc_eq_le car by auto
  with baseOpen have "∃f. f:Pi(?B,λt. ?N`t) ∧ (∀t∈?B. f`t∈?N`t)" by blast
  then obtain f where f:"f:Pi(?B,λt. ?N`t)" and f2:"∀t∈?B. f`t∈?N`t" by auto
  {
    fix U
    assume "U∈T" and "U≠0"
    then obtain b where A1:"b∈B-{0}" and "b⊆U" using Top_1_2_L1 base by blast
    with f2 have "f`b∈U" by auto
    with A1 have "{f`b. b∈?B}∩U≠0" by auto
  }
  then have r:"∀U∈T. U≠0 ⟶ {f`b. b∈?B}∩U≠0" by auto
  have "{f`b. b∈?B}⊆⋃T" using f2 baseOpen by auto
  moreover
  with r have "Closure({f`b. b∈?B},T)=⋃T" using dense_int_open assms(3) by auto
  moreover
  have ffun:"f:?B→range(f)" using f range_of_fun by auto
  then have "f∈surj(?B,range(f))" using fun_is_surj by auto
  then have des1:"range(f)≲?B" using surj_fun_inv_2[of "f""?B""range(f)""Q"] prec Card_less_csucc_eq_le car
    Card_is_Ord by auto
  then have "{f`b. b∈?B}⊆range(f)" using apply_rangeI[OF ffun] by auto
  then have "{f`b. b∈?B}≲range(f)" using subset_imp_lepoll by auto
  with des1 have "{f`b. b∈?B}≲?B" using lepoll_trans by blast
  with prec have "{f`b. b∈?B}≺csucc(Q)" using lesspoll_trans1 by auto
  ultimately show ?thesis using IsSeparableOfCard_def by auto
qed

text{*The next theorem resolves that the axiom of @{text "Q"} choice for subsets
of @{text "⋃T"} is necessary for second type spaces to be separable of the same cardinal
@{text "csucc(Q)"}.*}

theorem second_imp_separable_imp_Q_choice:
  assumes "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ (T{is separable of cardinal}csucc(Q))" 
  and "Card(Q)"
  shows "{the axiom of} Q {choice holds}"
proof-
  {
    fix N M
    assume AS:"M ≲Q ∧  (∀t∈M. N`t≠0)"
    (* First we build a topology using N and M such that it is of 
    second type of cardinal csucc(Q). It will be a partition topology.*)
    then obtain h where inj:"h∈inj(M,Q)" using lepoll_def by auto
    then have bij:"converse(h):bij(range(h),M)" using inj_bij_range bij_converse_bij by auto
    let ?T="{(N`(converse(h)`i))×{i}. i∈range(h)}"
    {
      fix j
      assume AS2:"j∈range(h)"
      from bij have "converse(h):range(h)→M" using bij_def inj_def by auto
      with AS2 have "converse(h)`j∈M" by simp
      with AS have "N`(converse(h)`j)≠0" by auto
      then have "(N`(converse(h)`j))×{j}≠0" by auto
    }
    then have noEmpty:"0∉?T" by auto
    moreover
    {
      fix A B
      assume AS2:"A∈?T""B∈?T""A∩B≠0"
      then obtain j t where A_def:"A=N`(converse(h)`j)×{j}" and B_def:"B=N`(converse(h)`t)×{t}"
        and Range:"j∈range(h)" "t∈range(h)" by auto
      from AS2(3) obtain x where "x∈A∩B" by auto
      with A_def B_def have "j=t" by auto
      with A_def B_def have "A=B" by auto
    }
    then have "(∀A∈?T. ∀B∈?T. A=B∨ A∩B=0)" by auto
    ultimately
    have Part:"?T {is a partition of} ⋃?T" unfolding IsAPartition_def by auto
    let ="PTopology ⋃?T ?T"
    from Part have top:"?τ {is a topology}" and base:"?T {is a base for}?τ"
      using Ptopology_is_a_topology by auto
    let ?f="{⟨i,(N`(converse(h)`i))×{i}⟩. i∈range(h)}" 
    have "?f:range(h)→?T" using functionI[of "?f"] Pi_def by auto
    then have "?f∈surj(range(h),?T)" unfolding surj_def using apply_equality by auto
    moreover
    have "range(h)⊆Q" using inj unfolding inj_def range_def domain_def Pi_def by auto
    ultimately have "?T≲ Q" using surj_fun_inv[of "?f""range(h)""?T""Q"] assms(2) Card_is_Ord lepoll_trans
      subset_imp_lepoll by auto
    then have  "?T≺csucc(Q)" using Card_less_csucc_eq_le assms(2) by auto
    with base have "(?τ{is of second type of cardinal}csucc(Q))" using IsSecondOfCard_def by auto
    with top have "?τ{is separable of cardinal}csucc(Q)" using assms(1) by auto
    then obtain D where sub:"D∈Pow(⋃?τ)" and clos:"Closure(D,?τ)=⋃?τ" and cardd:"D≺csucc(Q)"
      using IsSeparableOfCard_def by auto
    (*We now build a dense subset of D such that it has only one point in each
    basic set. The first coordinate of those points will give us a choice function.*)
    then have "D≲Q" using Card_less_csucc_eq_le assms(2) by auto
    then obtain r where r:"r∈inj(D,Q)" using lepoll_def by auto
    then have bij2:"converse(r):bij(range(r),D)" using inj_bij_range bij_converse_bij by auto
    then have surj2:"converse(r):surj(range(r),D)" using bij_def by auto
    let ?R="λi∈range(h). {j∈range(r). converse(r)`j∈((N`(converse(h)`i))×{i})}"
    {
      fix i
      assume AS:"i∈range(h)"
      then have T:"(N`(converse(h)`i))×{i}∈?T" by auto 
      then have op:"(N`(converse(h)`i))×{i}∈?τ" using base unfolding IsAbaseFor_def by blast
      with top sub clos have "∀U∈?τ. U≠0 ⟶ D∩U≠0" using dense_int_open by auto
      with op have "(N`(converse(h)`i))×{i}≠0 ⟶ D∩(N`(converse(h)`i))×{i}≠0" by auto
      with T noEmpty have "D∩(N`(converse(h)`i))×{i}≠0" by auto
      then obtain x where "x∈D" and px:"x∈(N`(converse(h)`i))×{i}" by auto
      with surj2 obtain j where "j∈range(r)" and "converse(r)`j=x" unfolding surj_def by blast
      with px have "j∈{j∈range(r). converse(r)`j∈((N`(converse(h)`i))×{i})}" by auto
      then have "?R`i≠0" using beta_if[of "range(h)" _ i] AS by auto
    }
    then have nonE:"∀i∈range(h). ?R`i≠0" by auto
    {
      fix i j
      assume i:"i∈range(h)" and j:"j∈?R`i"
      from j i have "converse(r)`j∈((N`(converse(h)`i))×{i})" using beta_if by auto
    }
    then have pp:"∀i∈range(h). ∀j∈?R`i. converse(r)`j∈((N`(converse(h)`i))×{i})" by auto
    let ?E="{⟨m,fst(converse(r)`(μ j. j∈?R`(h`m)))⟩. m∈M}"
    have ff:"function(?E)" unfolding function_def by auto
    moreover
    (*We now have to prove that ?E is a choice function for M and N*)
    {
      fix m
      assume M:"m∈M"
      with inj have hm:"h`m∈range(h)" using apply_rangeI inj_def by auto
      {
        fix j
        assume "j∈?R`(h`m)"
        with hm have "j∈range(r)" using beta_if by auto
        from r have "r:surj(D,range(r))" using fun_is_surj inj_def by auto
        with `j∈range(r)` obtain d where "d∈D" and "r`d=j" using surj_def by auto
        then have "j∈Q" using r inj_def by auto
      }
      then have subcar:"?R`(h`m)⊆Q" by blast
      from nonE hm obtain ee where P:"ee∈?R`(h`m)" by blast
      with subcar have "ee∈Q" by auto
      then have "Ord(ee)" using assms(2) Card_is_Ord Ord_in_Ord by auto
      with P have "(μ j. j∈?R`(h`m))∈?R`(h`m)" using LeastI[where i=ee and P="λj. j∈?R`(h`m)"]
      by auto
      with pp hm have "converse(r)`(μ j. j∈?R`(h`m))∈((N`(converse(h)`(h`m)))×{(h`m)})" by auto
      then have "converse(r)`(μ j. j∈?R`(h`m))∈((N`(m))×{(h`m)})" using left_inverse[OF inj M]
        by simp
      then have "fst(converse(r)`(μ j. j∈?R`(h`m)))∈(N`(m))" by auto
      }
    ultimately have thesis1:"∀m∈M. ?E`m∈(N`(m))" using function_apply_equality by auto
    {
      fix e
      assume "e∈?E"
      then obtain m where "m∈M" and "e=⟨m,?E`m⟩" using function_apply_equality ff by auto
      with thesis1 have "e∈Sigma(M,λt. N`t)" by auto
    }
    then have "?E∈Pow(Sigma(M,λt. N`t))" by auto
    with ff have "?E∈Pi(M,λm. N`m)" using Pi_iff by auto
    then have "(∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using thesis1 by auto
  }
  then show ?thesis using AxiomCardinalChoiceGen_def assms(2) by auto
qed

text{*Here is the equivalence from the two previous results.*}

theorem Q_choice_eq_secon_imp_sepa:
  assumes "Card(Q)"
  shows "(∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ (T{is separable of cardinal}csucc(Q)))
    ⟷({the axiom of} Q {choice holds})"
  using Q_choice_imp_second_imp_separable choice_subset_imp_choice
  using second_imp_separable_imp_Q_choice assms by auto

text{*Given a base injective with a set, then we can find a
base whose elements are indexed by that set.*}

lemma base_to_indexed_base:
  assumes "B ≲Q" "B {is a base for}T"
  shows "∃N. {N`i. i∈Q}{is a base for}T"
proof-
  from assms obtain f where f_def:"f∈inj(B,Q)" unfolding lepoll_def by auto
  let ?ff="{⟨b,f`b⟩. b∈B}"
  have "domain(?ff)=B" by auto
  moreover
  have "relation(?ff)" unfolding relation_def by auto
  moreover
  have "function(?ff)" unfolding function_def by auto
  ultimately
  have fun:"?ff:B→range(?ff)" using function_imp_Pi[of "?ff"] by auto
  then have injj:"?ff∈inj(B,range(?ff))" unfolding inj_def
  proof
    {
      fix w x
      assume AS:"w∈B""x∈B""{⟨b, f ` b⟩ . b ∈ B} ` w = {⟨b, f ` b⟩ . b ∈ B} ` x"
      then have "f`w=f`x" using apply_equality[OF _ fun] by auto
      then have "w=x" using f_def inj_def AS(1,2) by auto
    }
    then show "∀w∈B. ∀x∈B. {⟨b, f ` b⟩ . b ∈ B} ` w = {⟨b, f ` b⟩ . b ∈ B} ` x ⟶ w = x" by auto
  qed
  then have bij:"?ff∈bij(B,range(?ff))" using inj_bij_range by auto
  from fun have "range(?ff)={f`b. b∈B}" by auto
  with f_def have ran:"range(?ff)⊆Q" using inj_def by auto
  let ?N="{⟨i,(if i∈range(?ff) then converse(?ff)`i else 0)⟩. i∈Q}"
  have FN:"function(?N)" unfolding function_def by auto
  have "B ⊆{?N`i. i∈Q}"
  proof
    fix t
    assume a:"t∈B"
    from bij have rr:"?ff:B→range(?ff)" unfolding bij_def inj_def by auto
    have ig:"?ff`t=f`t" using a apply_equality[OF _ rr] by auto
    have r:"?ff`t∈range(?ff)" using apply_type[OF rr a].
    from ig have t:"?ff`t∈Q" using apply_type[OF _ a] f_def unfolding inj_def by auto
    with r have "?N`(?ff`t)=converse(?ff)`(?ff`t)" using function_apply_equality[OF _ FN] by auto
    then have "?N`(?ff`t)=t" using left_inverse[OF injj a] by auto
    then have "t=?N`(?ff`t)" by auto
    then have "∃i∈Q. t=?N`i" using t(1) by auto
    then show "t∈{?N`i. i∈Q}" by simp
  qed
  moreover
  have "∀r∈{?N`i. i∈Q}-B. r=0"
  proof
    fix r
    assume "r∈{?N`i. i∈Q}-B"
    then obtain j where R:"j∈Q""r=?N`j""r∉B" by auto
    {
      assume AS:"j∈range(?ff)"
      with R(1) have "?N`j=converse(?ff)`j" using function_apply_equality[OF _ FN] by auto
      then have "?N`j∈B" using  apply_funtype[OF inj_is_fun[OF bij_is_inj[OF bij_converse_bij[OF bij]]] AS]
      by auto
      then have "False" using R(3,2) by auto
    }
    then have "j∉range(?ff)" by auto
    then show "r=0" using function_apply_equality[OF _ FN] R(1,2) by auto
  qed
  ultimately have "{?N`i. i∈Q}=B∨{?N`i. i∈Q}=B ∪{0}" by blast
  moreover
  have "(B ∪{0})-{0}=B-{0}" by blast
  then have "(B ∪{0})-{0} {is a base for}T" using base_no_0[of "B""T"] assms(2) by auto
  then have "B ∪{0} {is a base for}T" using base_no_0[of "B ∪{0}""T"] by auto
  ultimately
  have "{?N`i. i∈Q}{is a base for}T" using assms(2) by auto
  then show ?thesis by auto
qed

subsection{*Relation between numerability and compactness*}  

text{*If the axiom of @{text "Q"} choice holds, then any topology
of second type of cardinal @{text "csucc(Q)"} is compact of cardinal @{text "csucc(Q)"}*}

theorem compact_of_cardinal_Q:
  assumes "{the axiom of} Q {choice holds for subsets} (Pow(Q))"
    "T{is of second type of cardinal}csucc(Q)"
    "T{is a topology}"
  shows "((⋃T){is compact of cardinal}csucc(Q){in}T)"
proof-
  from assms(1) have CC:"Card(Q)" and reg:"⋀ M N. (M ≲Q ∧ (∀t∈M. N`t≠0∧N`t⊆Pow(Q))) ⟶ (∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using
  AxiomCardinalChoice_def by auto
  from assms(2) obtain R where "R≲Q""R{is a base for}T" unfolding IsSecondOfCard_def using Card_less_csucc_eq_le CC by auto
  with base_to_indexed_base obtain N where base:"{N`i. i∈Q}{is a base for}T"  by blast
  {
    fix M
    assume A:"⋃T⊆⋃M""M∈Pow(T)"
    let ="λU∈M. {i∈Q. N`(i)⊆U}"
    have inj:"?α∈inj(M,Pow(Q))" unfolding inj_def
    proof
    {
      show "(λU∈M. {i ∈ Q . N ` i ⊆ U}) ∈ M → Pow(Q)" using lam_type[of "M""λU. {i ∈ Q . N`(i) ⊆ U}""%t. Pow(Q)"] by auto
      {
        fix w x
        assume AS:"w∈M""x∈M""{i ∈ Q . N`(i) ⊆ w} = {i ∈ Q . N`(i) ⊆ x}"
        from AS(1,2) A(2) have "w∈T""x∈T" by auto
        then have "w=Interior(w,T)""x=Interior(x,T)" using assms(3) topology0.Top_2_L3[of "T"]
          topology0_def[of "T"] by auto
        then have UN:"w=(⋃{B∈{N`(i). i∈Q}. B⊆w})""x=(⋃{B∈{N`(i). i∈Q}. B⊆x})"
          using interior_set_base_topology assms(3) base by auto
        {
          fix b
          assume "b∈w"
          then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆w}" using UN(1) by auto
          then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆w" by blast
          then obtain j where j:"j∈Q""S=N`(j)" by auto
          then have "j∈{i ∈ Q . N`(i) ⊆ w}" using S(3) by auto
          then have "N`(j)⊆x""b∈N`(j)""j∈Q" using S(2) AS(3) j by auto
          then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆x})" by auto
          then have "b∈x" using UN(2) by auto
        }
        moreover
        {
          fix b
          assume "b∈x"
          then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆x}" using UN(2) by auto
          then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆x" by blast
          then obtain j where j:"j∈Q""S=N`(j)" by auto
          then have "j∈{i ∈ Q . N`(i) ⊆ x}" using S(3) by auto
          then have "j∈{i ∈ Q . N`(i) ⊆ w}" using AS(3) by auto
          then have "N`(j)⊆w""b∈N`(j)""j∈Q" using S(2) j(2) by auto
          then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆w})" by auto
          then have "b∈w" using UN(2) by auto
        }
        ultimately have "w=x" by auto
      }
      then show "∀w∈M. ∀x∈M. (λU∈M. {i ∈ Q . N ` i ⊆ U}) ` w = (λU∈M. {i ∈ Q . N ` i ⊆ U}) ` x ⟶ w = x" by auto
    }
    qed
    let ?X="λi∈Q. {?α`U. U∈{V∈M. N`(i)⊆V}}"
    let ?M="{i∈Q. ?X`i≠0}"
    have subMQ:"?M⊆Q" by auto
    then have ddd:"?M ≲Q" using subset_imp_lepoll by auto
    then have "?M ≲Q""∀i∈?M. ?X`i≠0""∀i∈?M. ?X`i⊆Pow(Q)" by auto
    then have "?M ≲Q""∀i∈?M. ?X`i≠0""∀i∈?M. ?X`i ≲ Pow(Q)" using subset_imp_lepoll by auto
    then have "(∃f. f:Pi(?M,λt. ?X`t) ∧ (∀t∈?M. f`t∈?X`t))" using reg[of "?M""?X"] by auto
    then obtain f where f:"f:Pi(?M,λt. ?X`t)""(!!t. t∈?M ⟹ f`t∈?X`t)" by auto
    {
      fix m
      assume S:"m∈?M"
      from f(2) S obtain YY where YY:"(YY∈M)" "(f`m=?α`YY)" by auto
      then have Y:"(YY∈M)∧(f`m=?α`YY)" by auto
      moreover
      { 
        fix U
        assume "U∈M∧(f`m=?α`U)"
        then have "U=YY" using inj inj_def YY by auto
      }
      then have r:"⋀x. x∈M∧(f`m=?α`x) ⟹ x=YY" by blast
      have "∃!YY. YY∈M ∧ f`m=?α`YY" using ex1I[of "%Y. Y∈M∧ f`m=?α`Y",OF Y r] by auto
    }
    then have ex1YY:"∀m∈?M. ∃!YY. YY∈M ∧ f`m=?α`YY" by auto
    let ?YYm="{⟨m,(THE YY. YY∈M ∧ f`m=?α`YY)⟩. m∈?M}"
    have aux:"⋀m. m∈?M ⟹ ?YYm`m=(THE YY. YY∈M ∧ f`m=?α`YY)" unfolding apply_def by auto
    have ree:"∀m∈?M. (?YYm`m)∈M ∧ f`m=?α`(?YYm`m)"
    proof
      fix m
      assume C:"m∈?M"
      then have "∃!YY. YY∈M ∧ f`m=?α`YY" using ex1YY by auto
      then have "(THE YY. YY∈M ∧ f`m=?α`YY)∈M∧f`m=?α`(THE YY. YY∈M ∧ f`m=?α`YY)"
        using theI[of "%Y. Y∈M∧ f`m=?α`Y"] by blast
      then show "(?YYm`m)∈M ∧ f`m=?α`(?YYm`m)" apply (simp only: aux[OF C]) done
    qed
    have tt:"⋀m. m∈?M ⟹ N`(m)⊆?YYm`m"
    proof-
      fix m
      assume D:"m∈?M"
      then have QQ:"m∈Q" by auto
      from D have t:"(?YYm`m)∈M ∧ f`m=?α`(?YYm`m)" using ree by blast
      then have "f`m=?α`(?YYm`m)" by blast
      then have "(?α`(?YYm`m))∈(λi∈Q. {?α`U. U∈{V∈M. N`(i)⊆V}})`m" using f(2)[OF D]
        by auto
      then have "(?α`(?YYm`m))∈{?α`U. U∈{V∈M. N`(m)⊆V}}" using QQ by auto
      then obtain U where "U∈{V∈M. N`(m)⊆V}""?α`(?YYm`m)=?α`U" by auto
      then have r:"U∈M""N`(m)⊆U""?α`(?YYm`m)=?α`U""(?YYm`m)∈M" using t by auto
      then have "?YYm`m=U" using  inj_apply_equality[OF inj] by blast
      then show "N`(m)⊆?YYm`m" using r by auto
    qed
    then have "(⋃m∈?M. N`(m))⊆(⋃m∈?M. ?YYm`m)"
    proof-
      {
        fix s
        assume "s∈(⋃m∈?M. N`(m))"
        then obtain t where r:"t∈?M""s∈N`(t)" by auto
        then have "s∈?YYm`t" using tt[OF r(1)] by blast
        then have "s∈(⋃m∈?M. ?YYm`m)" using r(1) by blast
      }
      then show ?thesis by blast
    qed
    moreover
    {
      fix x
      assume AT:"x∈⋃T"
      with A obtain U where BB:"U∈M""U∈T""x∈U" by auto
      then obtain j where BC:"j∈Q" "N`(j)⊆U""x∈N`(j)" using point_open_base_neigh[OF base,of "U""x"] by auto
      then have "?X`j≠0" using BB(1) by auto
      then have "j∈?M" using BC(1) by auto
      then have "x∈(⋃m∈?M. N`(m))" using BC(3) by auto
    }
    then have "⋃T⊆(⋃m∈?M. N`(m))" by blast
    ultimately have covers:"⋃T⊆(⋃m∈?M. ?YYm`m)" using subset_trans[of "⋃T""(⋃m∈?M. N`(m))""(⋃m∈?M. ?YYm`m)"]
      by auto
    have "relation(?YYm)" unfolding relation_def by auto
    moreover
    have f:"function(?YYm)" unfolding function_def by auto
    moreover
    have d:"domain(?YYm)=?M" by auto
    moreover
    have r:"range(?YYm)=?YYm``?M" by auto
    ultimately
    have fun:"?YYm:?M→?YYm``?M" using function_imp_Pi[of "?YYm"] by auto
    have "?YYm∈surj(?M,?YYm``?M)" using fun_is_surj[OF fun] r by auto
    with surj_fun_inv[OF this subMQ Card_is_Ord[OF CC]]
    have "?YYm``?M ≲ ?M" by auto
    with ddd have Rw:"?YYm``?M ≲Q" using lepoll_trans by blast
    {
      fix m assume "m∈?M"
      then have "⟨m,?YYm`m⟩∈?YYm" using function_apply_Pair[OF f] d by blast
      then have "?YYm`m∈?YYm``?M" by auto}
      then have l1:"{?YYm`m. m∈?M}⊆?YYm``?M" by blast
      {
        fix t assume "t∈?YYm``?M"
        then have "∃x∈?M. ⟨x,t⟩∈?YYm" unfolding image_def by auto
        then obtain r where S:"r∈?M""⟨r,t⟩∈?YYm" by auto
        have "?YYm`r=t" using apply_equality[OF S(2) fun] by auto
        with S(1) have "t∈{?YYm`m. m∈?M}" by auto
      }
      with l1 have "{?YYm`m. m∈?M}=?YYm``?M" by blast
      with Rw have "{?YYm`m. m∈?M} ≲Q" by auto
      with covers have "{?YYm`m. m∈?M}∈Pow(M)∧⋃T⊆⋃{?YYm`m. m∈?M}∧{?YYm`m. m∈?M} ≺csucc(Q)" using ree 
        Card_less_csucc_eq_le[OF CC] by blast
      then have "∃N∈Pow(M). ⋃T⊆⋃N∧N≺csucc(Q)" by auto
    }
  then have "∀M∈Pow(T). ⋃T ⊆ ⋃M ⟶ (∃N∈Pow(M). ⋃T ⊆ ⋃N ∧ N ≺ csucc(Q))" by auto
  then show ?thesis using IsCompactOfCard_def Card_csucc CC Card_is_Ord by auto
qed

text{*In the following proof, we have chosen an infinite cardinal
to be able to apply the equation @{prop "Q×Q≈Q"}. For finite cardinals;
both, the assumption and the axiom of choice, are always true.*}

theorem second_imp_compact_imp_Q_choice_PowQ:
  assumes "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T)" 
  and "InfCard(Q)"
  shows "{the axiom of} Q {choice holds for subsets} (Pow(Q))"
proof-
  {
    fix N M
    assume AS:"M ≲Q ∧  (∀t∈M. N`t≠0 ∧ N`t⊆Pow(Q))"
    then obtain h where "h∈inj(M,Q)" using lepoll_def by auto
    (* First we build a topology that it is of second type 
    of cardinal csucc(Q). It will be a discrete topology.*)
    have discTop:"Pow(Q×M) {is a topology}" using Pow_is_top by auto
    {
      fix A
      assume AS:"A∈Pow(Q×M)"
      have "A=⋃{{i}. i∈A}" by auto
      with AS have "∃T∈Pow({{i}. i∈Q×M}). A=⋃T" by auto
      then have "A∈{⋃U. U∈Pow({{i}. i∈Q×M})}" by auto
    }
    moreover
    {
      fix A
      assume AS:"A∈{⋃U. U∈Pow({{i}. i∈Q×M})}"
      then have "A∈Pow(Q×M)" by auto
    }
    ultimately
    have base:"{{x}. x∈Q×M} {is a base for} Pow(Q×M)" unfolding IsAbaseFor_def by blast
    let ?f="{⟨i,{i}⟩. i∈Q×M}"
    have fff:"?f∈Q×M→{{i}. i∈Q×M}" using Pi_def function_def by auto
    then have "?f∈inj(Q×M,{{i}. i∈Q×M})" unfolding inj_def using apply_equality by auto
    then have "?f∈bij(Q×M,{{i}. i∈Q×M})" unfolding bij_def surj_def  using fff
      apply_equality fff by auto
    then have "Q×M≈{{i}. i∈Q×M}" using eqpoll_def by auto
    then have "{{i}. i∈Q×M}≈Q×M" using eqpoll_sym by auto
    then have "{{i}. i∈Q×M}≲Q×M" using eqpoll_imp_lepoll by auto
    then have "{{i}. i∈Q×M}≲Q×Q" using AS prod_lepoll_mono[of "Q""Q""M""Q"] lepoll_refl[of "Q"]
      lepoll_trans by blast
    then have "{{i}. i∈Q×M}≲Q" using InfCard_square_eqpoll assms(2) lepoll_eq_trans by auto
    then have "{{i}. i∈Q×M}≺csucc(Q)" using Card_less_csucc_eq_le assms(2) InfCard_is_Card by auto
    then have "Pow(Q×M) {is of second type of cardinal} csucc(Q)" using IsSecondOfCard_def base by auto
    then have comp:"(Q×M) {is compact of cardinal}csucc(Q){in}Pow(Q×M)" using discTop assms(1) by auto
    {
      fix W
      assume "W∈Pow(Q×M)"
      then have T:"W{is closed in} Pow(Q×M)" and "(Q×M)∩W=W" using IsClosed_def by auto
      with compact_closed[OF comp T] have "(W {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
    }
    then have subCompact:"∀W∈Pow(Q×M). (W {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
    let ?cub="⋃{{(U)×{t}. U∈N`t}. t∈M}"
    from AS have "(⋃?cub)∈Pow((Q)×M)" by auto
    with subCompact have Ncomp:"((⋃?cub) {is compact of cardinal}csucc(Q){in}Pow(Q×M))" by auto
    have cond:"(?cub)∈Pow(Pow(Q×M))∧ ⋃?cub⊆⋃?cub" using AS by auto
    have "∃S∈Pow(?cub). (⋃?cub) ⊆ ⋃S ∧ S ≺ csucc(Q)"
    proof-
      {
        have "((⋃?cub) {is compact of cardinal}csucc(Q){in}Pow(Q×M))" using Ncomp by auto
        then have "∀M∈Pow(Pow(Q×M)). ⋃?cub ⊆ ⋃M ⟶ (∃Na∈Pow(M). ⋃?cub ⊆ ⋃Na ∧ Na ≺ csucc(Q))" 
          unfolding IsCompactOfCard_def by auto
        with cond have "∃S∈Pow(?cub). ⋃?cub ⊆ ⋃S ∧ S ≺ csucc(Q)" by auto
      }
      then show ?thesis by auto
    qed
    then have ttt:"∃S∈Pow(?cub). (⋃?cub) ⊆ ⋃S ∧ S ≲ Q" using Card_less_csucc_eq_le assms(2) InfCard_is_Card by auto
    then obtain S where S_def:"S∈Pow(?cub)""(⋃?cub) ⊆ ⋃S" "S ≲ Q" by auto
    {
      fix t
      assume AA:"t∈M""N`t≠{0}"
      from AA(1) AS have "N`t≠0" by auto
      with AA(2) obtain U where G:"U∈N`t" and notEm:"U≠0" by blast
      then have "U×{t}∈?cub" using AA by auto
      then have "U×{t}⊆⋃?cub" by auto
      with G notEm AA have "∃s. ⟨s,t⟩∈⋃?cub" by auto
    }
    then have "∀t∈M. (N`t≠{0})⟶ (∃s. ⟨s,t⟩∈⋃?cub)" by auto
    then have A:"∀t∈M. (N`t≠{0})⟶ (∃s. ⟨s,t⟩∈⋃S)" using S_def(2) by blast
    from S_def(1) have B:"∀f∈S. ∃t∈M. ∃U∈N`t. f=U×{t}" by blast
    from A B have "∀t∈M. (N`t≠{0})⟶ (∃U∈N`t. U×{t}∈S)" by blast
    then have noEmp:"∀t∈M. (N`t≠{0})⟶ (S∩({U×{t}. U∈N`t})≠0)" by auto
    from S_def(3) obtain r where r:"r:inj(S,Q)" using lepoll_def by auto
    then have bij2:"converse(r):bij(range(r),S)" using inj_bij_range bij_converse_bij by auto
    then have surj2:"converse(r):surj(range(r),S)" using bij_def by auto
    let ?R="λt∈M. {j∈range(r). converse(r)`j∈({U×{t}. U∈N`t})}"
    {
      fix t
      assume AA:"t∈M""N`t≠{0}"
      then have "(S∩({U×{t}. U∈N`t})≠0)" using noEmp by auto
      then obtain s where ss:"s∈S""s∈{U×{t}. U∈N`t}" by blast
      then obtain j where "converse(r)`j=s" "j∈range(r)" using surj2 unfolding surj_def by blast
      then have "j∈{j∈range(r). converse(r)`j∈({U×{t}. U∈N`t})}" using ss by auto
      then have "?R`t≠0" using beta_if AA by auto
    }
    then have nonE:"∀t∈M. N`t≠{0}⟶?R`t≠0" by auto
    {
      fix t j
      assume "t∈M""j∈?R`t"
      then have "converse(r)`j∈{U×{t}. U∈N`t}" using beta_if by auto
      }
    then have pp:"∀t∈M. ∀j∈?R`t. converse(r)`j∈{U×{t}. U∈N`t}" by auto
    have reg:"∀t U V. U×{t}=V×{t}⟶U=V"
    proof-
      { 
        fix t U V
        assume AA:"U×{t}=V×{t}"
        {
          fix v
          assume "v∈V"
          then have "⟨v,t⟩∈V ×{t}" by auto
          then have "⟨v,t⟩∈U ×{t}" using AA by auto
          then have "v∈U" by auto
        }
        then have "V⊆U" by auto
        moreover
        {
          fix u
          assume "u∈U"
          then have "⟨u,t⟩∈U ×{t}" by auto
          then have "⟨u,t⟩∈V ×{t}" using AA by auto
          then have "u∈V" by auto
        }
        then have "U⊆V" by auto
        ultimately have "U=V" by auto
      }
      then show ?thesis by auto
    qed
    (*The last part is to prove that ?E is the choice function.*)
    let ?E="{⟨t,if N`t={0} then 0 else (THE U. converse(r)`(μ j. j∈?R`t)=U×{t})⟩. t∈M}"
    have ff:"function(?E)" unfolding function_def by auto
    moreover
    {
      fix t
      assume pm:"t∈M"
       { assume nonEE:"N`t≠{0}"
      {
        fix j
        assume "j∈?R`t"
        with pm(1) have "j∈range(r)" using beta_if by auto
        from r have "r:surj(S,range(r))" using fun_is_surj inj_def by auto
        with `j∈range(r)` obtain d where "d∈S" and "r`d=j" using surj_def by auto
        then have "j∈Q" using r inj_def by auto
        }
      then have sub:"?R`t⊆Q" by blast
      from nonE pm nonEE obtain ee where P:"ee∈?R`t" by blast
      with sub have "ee∈Q" by auto
      then have "Ord(ee)" using assms(2) Card_is_Ord Ord_in_Ord InfCard_is_Card by blast
      with P have "(μ j. j∈?R`t)∈?R`t" using LeastI[where i=ee and P="λj. j∈?R`t"] by auto
      with pp pm have "converse(r)`(μ j. j∈?R`t)∈{U×{t}. U∈N`t}" by auto
      then obtain W where "converse(r)`(μ j. j∈?R`t)=W×{t}" and s:"W∈N`t" by auto
      then have "(THE U. converse(r)`(μ j. j∈?R`t)=U×{t})=W" using reg by auto
      with s have "(THE U. converse(r)`(μ j. j∈?R`t)=U×{t})∈N`t" by auto
    }
    then have "(if N`t={0} then 0 else (THE U. converse(r)`(μ j. j∈?R`t)=U×{t}))∈N`t" by auto
    }
    ultimately have thesis1:"∀t∈M. ?E`t∈N`t" using function_apply_equality by auto
    {
      fix e
      assume "e∈?E"
      then obtain m where "m∈M" and "e=⟨m,?E`m⟩" using function_apply_equality ff by auto
      with thesis1 have "e∈Sigma(M,λt. N`t)" by auto
    }
    then have "?E∈Pow(Sigma(M,λt. N`t))" by auto
    with ff have "?E∈Pi(M,λm. N`m)" using Pi_iff by auto
    then have "(∃f. f:Pi(M,λt. N`t) ∧ (∀t∈M. f`t∈N`t))" using thesis1 by auto}
    then show ?thesis using AxiomCardinalChoice_def assms(2) InfCard_is_Card by auto
qed

text{*The two previous results, state the following equivalence:*}

theorem Q_choice_Pow_eq_secon_imp_comp:
  assumes "InfCard(Q)"
  shows  "(∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T))
    ⟷({the axiom of} Q {choice holds for subsets} (Pow(Q)))"
    using second_imp_compact_imp_Q_choice_PowQ compact_of_cardinal_Q assms by auto

text{*In the next result we will prove that if the space $(\kappa,Pow(\kappa))$,
for $\kappa$ an infinite cardinal, is compact of its successor cardinal; then all
topologycal spaces which are of second type of the successor cardinal of $\kappa$
are also compact of that cardinal.*}

theorem Q_csuccQ_comp_eq_Q_choice_Pow:
  assumes "InfCard(Q)" "(Q){is compact of cardinal}csucc(Q){in}Pow(Q)"
  shows "∀T. (T{is a topology} ∧ (T{is of second type of cardinal}csucc(Q))) ⟶ ((⋃T){is compact of cardinal}csucc(Q){in}T)"
proof
  fix T
  {
    assume top:"T {is a topology}" and sec:"T{is of second type of cardinal}csucc(Q)"
    from assms have "Card(csucc(Q))" "Card(Q)" using InfCard_is_Card Card_is_Ord Card_csucc by auto
    moreover
    have "⋃T⊆⋃T" by auto
    moreover
    {
      fix M
      assume MT:"M∈Pow(T)" and cover:"⋃T⊆⋃M"
      from sec obtain B where "B {is a base for} T" "B≺csucc(Q)" using IsSecondOfCard_def by auto
      with `Card(Q)` obtain N where base:"{N`i. i∈Q}{is a base for}T" using Card_less_csucc_eq_le
        base_to_indexed_base by blast
      let ?S="{⟨u,{i∈Q. N`i⊆u}⟩. u∈M}"
      have "function(?S)" unfolding function_def by auto
      then have "?S:M→Pow(Q)" using Pi_iff by auto
      then have "?S∈inj(M,Pow(Q))" unfolding inj_def
        proof
        {
          fix w x
          assume AS:"w∈M""x∈M""{⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` w = {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` x"
          with `?S:M→Pow(Q)` have ASS:"{i ∈ Q . N ` i ⊆ w}={i ∈ Q . N ` i ⊆ x}" using apply_equality by auto
          from AS(1,2) MT have "w∈T""x∈T" by auto
          then have "w=Interior(w,T)""x=Interior(x,T)" using top topology0.Top_2_L3[of "T"]
            topology0_def[of "T"] by auto
          then have UN:"w=(⋃{B∈{N`(i). i∈Q}. B⊆w})""x=(⋃{B∈{N`(i). i∈Q}. B⊆x})"
            using interior_set_base_topology top base by auto
          {
            fix b
            assume "b∈w"
            then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆w}" using UN(1) by auto
            then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆w" by blast
            then obtain j where j:"j∈Q""S=N`(j)" by auto
            then have "j∈{i ∈ Q . N`(i) ⊆ w}" using S(3) by auto
            then have "N`(j)⊆x""b∈N`(j)""j∈Q" using S(2) ASS j by auto
            then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆x})" by auto
            then have "b∈x" using UN(2) by auto
          }
          moreover
          {
            fix b
            assume "b∈x"
            then have "b∈⋃{B∈{N`(i). i∈Q}. B⊆x}" using UN(2) by auto
            then obtain S where S:"S∈{N`(i). i∈Q}" "b∈S" "S⊆x" by blast
            then obtain j where j:"j∈Q""S=N`(j)" by auto
            then have "j∈{i ∈ Q . N`(i) ⊆ x}" using S(3) by auto
            then have "j∈{i ∈ Q . N`(i) ⊆ w}" using ASS by auto
            then have "N`(j)⊆w""b∈N`(j)""j∈Q" using S(2) j(2) by auto
            then have "b∈(⋃{B∈{N`(i). i∈Q}. B⊆w})" by auto
            then have "b∈w" using UN(2) by auto
          }
          ultimately have "w=x" by auto 
        }
        then show "∀w∈M. ∀x∈M. {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` w = {⟨u, {i ∈ Q . N ` i ⊆ u}⟩ . u ∈ M} ` x ⟶ w = x" by auto
      qed
      then have "?S∈bij(M,range(?S))" using fun_is_surj unfolding bij_def inj_def surj_def by force
      have "range(?S)⊆Pow(Q)" by auto
      then have "range(?S)∈Pow(Pow(Q))" by auto
      moreover
      have "(⋃(range(?S))) {is closed in} Pow(Q)" "Q∩(⋃range(?S))=(⋃range(?S))" using IsClosed_def by auto
      from this(2) compact_closed[OF assms(2) this(1)] have "(⋃range(?S)){is compact of cardinal}csucc(Q) {in}Pow(Q)"
        by auto
      moreover
      have "⋃(range(?S))⊆⋃(range(?S))" by auto
      ultimately have "∃S∈Pow(range(?S)). (⋃(range(?S)))⊆⋃S ∧ S≺ csucc(Q)" using IsCompactOfCard_def by auto
      then obtain SS where SS_def:"SS⊆range(?S)" "(⋃(range(?S)))⊆⋃SS" "SS≺ csucc(Q)" by auto
      with `?S∈bij(M,range(?S))` have con:"converse(?S)∈bij(range(?S),M)" using bij_converse_bij by auto
      then have r1:"restrict(converse(?S),SS)∈bij(SS,converse(?S)``SS)" using restrict_bij bij_def SS_def(1) by auto
      then have rr:"converse(restrict(converse(?S),SS))∈bij(converse(?S)``SS,SS)" using bij_converse_bij by auto
      {
        fix x
        assume "x∈⋃T"
        with cover have "x∈⋃M" by auto
        then obtain R where "R∈M" "x∈R" by auto
        with MT have "R∈T" "x∈R" by auto
        then have "∃V∈{N`i. i∈Q}. V⊆R ∧ x∈V" using point_open_base_neigh base by force
        then obtain j where "j∈Q" "N`j⊆R" and x_p:"x∈N`j" by auto
        with `R∈M` `?S:M→Pow(Q)` `?S∈bij(M,range(?S))` have "?S`R∈range(?S) ∧ j∈?S`R" using apply_equality 
          bij_def inj_def by auto
        from exI[where P="λt. t∈range(?S) ∧ j∈t", OF this] have "∃A∈range(?S). j∈A" unfolding Bex_def
          by auto
        then have "j∈(⋃(range(?S)))" by auto
        then have "j∈⋃SS" using SS_def(2) by blast
        then obtain SR where "SR∈SS" "j∈SR" by auto
        moreover
        have "converse(restrict(converse(?S),SS))∈surj(converse(?S)``SS,SS)" using rr bij_def by auto
        ultimately obtain RR where "converse(restrict(converse(?S),SS))`RR=SR" and p:"RR∈converse(?S)``SS" unfolding surj_def by blast
        then have "converse(converse(restrict(converse(?S),SS)))`(converse(restrict(converse(?S),SS))`RR)=converse(converse(restrict(converse(?S),SS)))`SR"
          by auto
        moreover
        have "converse(restrict(converse(?S),SS))∈inj(converse(?S)``SS,SS)" using rr unfolding bij_def by auto
        moreover
        ultimately have "RR=converse(converse(restrict(converse(?S),SS)))`SR" using left_inverse[OF _ p]
          by force
        moreover
        with r1 have "restrict(converse(?S),SS)∈SS→converse(?S)``SS" unfolding bij_def inj_def by auto
        then have "relation(restrict(converse(?S),SS))" using Pi_def relation_def by auto
        then have "converse(converse(restrict(converse(?S),SS)))=restrict(converse(?S),SS)" using relation_converse_converse by auto
        ultimately have "RR=restrict(converse(?S),SS)`SR" by auto
        with `SR∈SS` have eq:"RR=converse(?S)`SR" unfolding restrict by auto
        then have "converse(converse(?S))`RR=converse(converse(?S))`(converse(?S)`SR)" by auto
        moreover
        with `SR∈SS` have "SR∈range(?S)" using SS_def(1) by auto
        from con left_inverse[OF _ this] have "converse(converse(?S))`(converse(?S)`SR)=SR" unfolding bij_def
          by auto
        ultimately have "converse(converse(?S))`RR=SR" by auto
        then have "?S`RR=SR" using relation_converse_converse[of "?S"] unfolding relation_def by auto
        moreover
        have "converse(?S):range(?S)→M" using con bij_def inj_def by auto
        with `SR∈range(?S)` have "converse(?S)`SR∈M" using apply_funtype
          by auto
        with eq have "RR∈M" by auto
        ultimately have "SR={i∈Q. N`i⊆RR}" using `?S:M→Pow(Q)` apply_equality by auto
        then have "N`j⊆RR" using `j∈SR` by auto
        with x_p have "x∈RR" by auto
        with p have "x∈⋃(converse(?S)``SS)" by auto
      }
      then have "⋃T⊆⋃(converse(?S)``SS)" by blast
      moreover
      {
        from con have "converse(?S)``SS={converse(?S)`R. R∈SS}" using image_function[of "converse(?S)" "SS"]
          SS_def(1) unfolding range_def bij_def inj_def Pi_def by auto
        have "{converse(?S)`R. R∈SS}⊆{converse(?S)`R. R∈range(?S)}" using SS_def(1) by auto
        moreover
        have "converse(?S):range(?S)→M" using con unfolding bij_def inj_def by auto
        then have "{converse(?S)`R. R∈range(?S)}⊆M" using apply_funtype by force
        ultimately
        have "(converse(?S)``SS)⊆M" by auto
      }
      then have "converse(?S)``SS∈Pow(M)" by auto
      moreover
      with rr have "converse(?S)``SS≈SS" using eqpoll_def by auto
      then have "converse(?S)``SS≺csucc(Q)" using SS_def(3) eq_lesspoll_trans by auto
      ultimately
      have "∃N∈Pow(M). ⋃T⊆⋃N ∧ N≺csucc(Q)" by auto
    }
    then have "∀M∈Pow(T). ⋃T⊆⋃M ⟶ (∃N∈Pow(M). ⋃T⊆⋃N ∧ N≺csucc(Q))" by auto
    ultimately have "(⋃T){is compact of cardinal}csucc(Q){in}T" unfolding IsCompactOfCard_def
      by auto
  }
  then show "(T {is a topology}) ∧ (T {is of second type of cardinal}csucc(Q)) ⟶ ((⋃T){is compact of cardinal}csucc(Q) {in}T)"
  by auto
qed

theorem Q_disc_is_second_card_csuccQ:
  assumes "InfCard(Q)" 
  shows "Pow(Q){is of second type of cardinal}csucc(Q)"
proof-
  {
    fix A
    assume AS:"A∈Pow(Q)"
    have "A=⋃{{i}. i∈A}" by auto
    with AS have "∃T∈Pow({{i}. i∈Q}). A=⋃T" by auto
    then have "A∈{⋃U. U∈Pow({{i}. i∈Q})}" by auto
  }
  moreover
  {
    fix A
    assume AS:"A∈{⋃U. U∈Pow({{i}. i∈Q})}"
    then have "A∈Pow(Q)" by auto
  }
  ultimately
  have base:"{{x}. x∈Q} {is a base for} Pow(Q)" unfolding IsAbaseFor_def by blast
  let ?f="{⟨i,{i}⟩. i∈Q}"
  have "?f∈Q→{{x}. x∈Q}" unfolding Pi_def function_def by auto
  then have "?f∈inj(Q,{{x}. x∈Q})" unfolding inj_def using apply_equality by auto
  moreover
  from `?f∈Q→{{x}. x∈Q}` have "?f∈surj(Q,{{x}. x∈Q})" unfolding surj_def using apply_equality
    by auto
  ultimately have "?f∈bij(Q,{{x}. x∈Q})" unfolding bij_def by auto
  then have "Q≈{{x}. x∈Q}" using eqpoll_def by auto
  then have "{{x}. x∈Q}≈Q" using eqpoll_sym by auto
  then have "{{x}. x∈Q}≲Q" using eqpoll_imp_lepoll by auto
  then have "{{x}. x∈Q}≺csucc(Q)" using Card_less_csucc_eq_le assms InfCard_is_Card by auto
  with base show ?thesis using IsSecondOfCard_def by auto
qed

text{*This previous results give us another equivalence of the axiom of @{text "Q"} choice
that is apparently weaker (easier to check) to the previous one.*}

theorem Q_disc_comp_csuccQ_eq_Q_choice_csuccQ:
  assumes "InfCard(Q)"
  shows "(Q{is compact of cardinal}csucc(Q){in}(Pow(Q))) ⟷ ({the axiom of}Q{choice holds for subsets}(Pow(Q)))"
  proof
  assume "Q{is compact of cardinal}csucc(Q) {in}Pow(Q)"
  with assms show "{the axiom of}Q{choice holds for subsets}(Pow(Q))" using Q_choice_Pow_eq_secon_imp_comp Q_csuccQ_comp_eq_Q_choice_Pow
    by auto
  next
  assume "{the axiom of}Q{choice holds for subsets}(Pow(Q))"
  with assms show "Q{is compact of cardinal}csucc(Q){in}(Pow(Q))" using Q_disc_is_second_card_csuccQ Q_choice_Pow_eq_secon_imp_comp Pow_is_top[of "Q"]
    by force
qed


end