Require Export Basics.

(* We assume a countable model of ZF with infinity *)

Section Uncountable.

  Variable set : ZFStruct.
  Hypothesis SZF : ZF set.
  Hypothesis SI : Inf set.

  Variable f : nat -> set.
  Hypothesis f_sur : forall x, exists n, f n = x.

  Definition om :=
    delta (fun om' => agree finpow om').

  Lemma Infinity' :
    agree finpow om.
  Proof.
    unfold om. destruct SI as [om' H].
    apply (delta_spec H). apply agree_unique.
  Qed.

  Definition Num x :=
    exists n, x = powit n.

  Lemma Infinity :
    agree Num om.
  Proof.
    intros x. rewrite (Infinity' x).
    split; intros [n H]; exists n; now apply ZFExt.
  Qed.

  Lemma powit_inj m n :
    powit m = powit n -> m = n.
  Proof.
    revert m. induction n; destruct m; simpl.
    - tauto.
    - intros H. apply inhab_not in H.
      exfalso. apply H. exists 0. apply Power. auto.
    - intros H. apply eq_sym, inhab_not in H.
      exfalso. apply H. exists 0. apply Power. auto.
    - intros H % power_inj.
      now rewrite (IHn m H).
  Qed.

  (* With a diagonalisation argument we derive a contradiction *)

  Definition N n :=
    (powit n) nel (f n).

  Definition M :=
    sep (fun x => exists n, powit n = x /\ N n) om.

  Lemma help n :
    f n = M -> (powit n nel M <-> (powit n el om /\ (exists m, powit m = powit n /\ N m))).
  Proof.
    intros H. split; intros I.
    - split.
      + apply Infinity. now exists n.
      + exists n. split; trivial. unfold N. now rewrite H.
    - intros J. destruct I as [I1[m[I2 I3]]].
      apply I3. apply powit_inj in I2. subst m. now rewrite H.
  Qed.

  Lemma false :
    False.
  Proof.
    destruct (f_sur M) as [n H].
    specialize (sep_el (fun x => exists n, powit n = x /\ N n) om).
    intros I. specialize (I (powit n)). fold N in I.
    apply help in H. tauto.
  Qed.

End Uncountable.