# Models of ZF with Infinity are uncountable

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.